Changes

Summary

misc tuning and modernization;
simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
tuned;
misc tuning and modernization;
discontinued old 'def' command;

Changeset 67123:3fe40ff1b921 by wenzelm: misc tuning and modernization;
The file was modified	`src/HOL/Decision_Procs/Algebra_Aux.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Commutative_Ring.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Commutative_Ring_Complete.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Cooper.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Rat_Pair.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Reflective_Field.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/ex/Commutative_Ring_Ex.thy` (diff)
Changeset 67122:85b40f300fab by wenzelm: simplified session (again, see 39e29972cb96): WordExamples requires < 1s;
The file was added	`src/HOL/Word/WordExamples.thy`
The file was modified	`src/HOL/ROOT` (diff)
The file was modified	`src/HOL/Word/Word.thy` (diff)
The file was removed	`src/HOL/Word/Examples/WordExamples.thy`
Changeset 67121:116968454d70 by wenzelm: tuned;
The file was modified	`src/HOL/Word/WordBitwise.thy` (diff)
Changeset 67120:491fd7f0b5df by wenzelm: misc tuning and modernization;
The file was modified	`src/HOL/Word/Bit_Comparison.thy` (diff)
The file was modified	`src/HOL/Word/Bits_Bit.thy` (diff)
The file was modified	`src/HOL/Word/Bits_Int.thy` (diff)
The file was modified	`src/HOL/Word/Bool_List_Representation.thy` (diff)
The file was modified	`src/HOL/Word/Misc_Typedef.thy` (diff)
The file was modified	`src/HOL/Word/WordBitwise.thy` (diff)
The file was modified	`src/HOL/Word/Word_Miscellaneous.thy` (diff)
Changeset 67119:acb0807ddb56 by wenzelm: discontinued old 'def' command;
The file was modified	`NEWS` (diff)
The file was modified	`src/Doc/Isar_Ref/Proof.thy` (diff)
The file was modified	`src/FOL/ex/Locale_Test/Locale_Test1.thy` (diff)
The file was modified	`src/Pure/Isar/proof.ML` (diff)
The file was modified	`src/Pure/Pure.thy` (diff)