NEWS: More uniform and scalable declarations of intro/elim/dest rules

[Florian Haftmann]

Just a side-remark:

> That further detail would require to go into the smt proof 
> reconstruction, to see where its invocations of fast_tac/blast_tac/ 
> auto_tac etc. actually fail, or rather consume much more time than 
> before --- and thus break (line 6705 of "$AFP/ 
> Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"), 
> for example.

I also stumbled over that proof and it can be dramatically simplified:

> -    have "A $$ (0, 0) = A'' $$ (0, 0)"
> -      by (smt (verit) add_gr_0 append_rows_def A_def A'' carrier_matD index_mat_four_block(1) mn n0 nat_SN.compat)
> +    from \<open>0 < n\<close> \<open>0 < m\<close> A'' have \<open>A $$ (0, 0) = A'' $$ (0, 0)\<close>
> +      by (simp add: A_def append_rows_def)

I will leave it »as it is« for the moment as long as it serves as an 
important indicator for smt proof reconstruction.

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250724/f0effea7/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250724/f0effea7/attachment.sig>