Changes

Summary

extraction of equations x = t from premises beneath meta-all
a small aggiornamento for Z2
removed superfluous dependency
factored out ancient numeral representation
moved to Word_Lib
more explicit proofs

Changeset 71989:bad75618fb82 by haftmann: extraction of equations x = t from premises beneath meta-all
The file was modified	`CONTRIBUTORS` (diff)
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Auth/Guard/P1.thy` (diff)
The file was modified	`src/HOL/Auth/Guard/P2.thy` (diff)
The file was modified	`src/HOL/Bali/DefiniteAssignmentCorrect.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AVL_Bal_Set.thy` (diff)
The file was modified	`src/HOL/HOL.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/Abstraction.thy` (diff)
The file was modified	`src/HOL/HOLCF/IOA/TLS.thy` (diff)
The file was modified	`src/HOL/Hoare/Pointer_Examples.thy` (diff)
The file was modified	`src/HOL/Hoare/Pointer_ExamplesAbort.thy` (diff)
The file was modified	`src/HOL/Hoare/Pointers0.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/RG_Hoare.thy` (diff)
The file was modified	`src/HOL/Hoare_Parallel/RG_Tran.thy` (diff)
The file was modified	`src/HOL/MicroJava/Comp/CorrCompTp.thy` (diff)
The file was modified	`src/HOL/MicroJava/J/WellForm.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Class1.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Class3.thy` (diff)
The file was modified	`src/HOL/Nominal/Examples/Standardization.thy` (diff)
The file was modified	`src/HOL/Probability/Random_Permutations.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Higman.thy` (diff)
The file was modified	`src/HOL/Proofs/Extraction/Warshall.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/LambdaType.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/WeakNorm.thy` (diff)
The file was modified	`src/HOL/ROOT` (diff)
The file was modified	`src/HOL/Word/Bits_Int.thy` (diff)
The file was removed	`src/HOL/Library/Quantified_Premise_Simproc.thy`
Changeset 71988:ace45a11a45e by haftmann: a small aggiornamento for Z2
The file was modified	`src/HOL/Library/Z2.thy` (diff)
Changeset 71987:ec17263ec38d by haftmann: removed superfluous dependency
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Word/Misc_Arithmetic.thy` (diff)
Changeset 71986:76193dd4aec8 by haftmann: factored out ancient numeral representation
The file was added	`src/HOL/Word/Ancient_Numeral.thy`
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Library/Bit_Operations.thy` (diff)
The file was modified	`src/HOL/Word/Bits_Int.thy` (diff)
The file was modified	`src/HOL/Word/More_Word.thy` (diff)
The file was modified	`src/HOL/Word/Word.thy` (diff)
Changeset 71985:a1cf296a7786 by haftmann: moved to Word_Lib
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Word/More_Word.thy` (diff)
The file was modified	`src/HOL/Word/Word_Examples.thy` (diff)
The file was removed	`src/HOL/Word/Word_Bitwise.thy`
Changeset 71984:10a8d943a8d8 by haftmann: more explicit proofs
The file was modified	`src/HOL/Word/Bits_Int.thy` (diff)