Changes

Summary

pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
updated CVC4 component to official 1.5 release
merged
eliminated more "guess", etc.
merged
more tidying
more tidying up
merged
merged
removed all "guess"
tuned
merged
added lemmas
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping; sufficient to keep history stamps rather than complete historized data; semantically conflicting specifications are temoprary blacklisted after theory merge but remain historized; clarified signature;
merged
generalized lemma

Changeset 66323:c41642bc1ebb by blanchet: pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better
The file was modified	`src/HOL/SMT.thy` (diff)
Changeset 66322:bdf4d5408b01 by blanchet: updated CVC4 component to official 1.5 release
The file was modified	`Admin/components/components.sha1` (diff)
The file was modified	`Admin/components/main` (diff)
Changeset 66321:ea6cbb69dda2 by paulson: merged
Changeset 66320:9786b06c7b5a by paulson _lp15@cam.ac.uk_: eliminated more "guess", etc.
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Integral_Substitution.thy` (diff)
Changeset 66319:b66e0e5941a2 by paulson: merged
Changeset 66318:f2e1047d6cc1 by paulson _lp15@cam.ac.uk_: more tidying
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)
Changeset 66317:a9bb833ee971 by paulson: more tidying up
The file was modified	`src/HOL/Analysis/Lebesgue_Integral_Substitution.thy` (diff)
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)
Changeset 66316:2a1739aad711 by paulson: merged
Changeset 66315:ce50687a700e by paulson: merged
Changeset 66314:52914a618299 by paulson: removed all "guess"
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)
Changeset 66313:604616b627f2 by nipkow: tuned
The file was modified	`src/HOL/Library/Multiset.thy` (diff)
Changeset 66312:9a4c049f8997 by nipkow: merged
Changeset 66311:037aaa0b6daf by nipkow: added lemmas
The file was modified	`src/HOL/Binomial.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Formal_Power_Series.thy` (diff)
The file was modified	`src/HOL/Groups_List.thy` (diff)
The file was modified	`src/HOL/Proofs/Lambda/ListApplication.thy` (diff)
Changeset 66310:e8d2862ec203 by haftmann: simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;<br>sufficient to keep history stamps rather than complete historized data;<br>semantically conflicting specifications are temoprary blacklisted after theory merge but remain historized;<br>clarified signature;
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Tools/code_evaluation.ML` (diff)
The file was modified	`src/Pure/Isar/code.ML` (diff)
Changeset 66309:ca985e87c123 by nipkow: merged
Changeset 66308:b6a0d95b94be by nipkow: generalized lemma
The file was modified	`src/HOL/Groups_List.thy` (diff)