Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned, continuing e955964d89cb;
  3. avoid waste of resources due to dynamic simpset (amending 45c09620f726);
  4. fix latex
  5. clarified modules;
  6. more generic bit/word lemmas for distribution
  7. merged
  8. Added / moved some simple set-theoretic lemmas
  9. more CONTRIBUTORS and NEWS;
  10. cleanup; add Apple reference
  11. refine interface
  12. generalized component lookup for syntax and distinctness proofs. added some tracing.
Changeset 74597:ea5d28c7f5e5 by wenzelm:
merged
Changeset 74596:55d4f8e1877f by wenzelm:
tuned, continuing e955964d89cb;
The file was modified src/Pure/ML/ml_thms.ML (diff)
Changeset 74595:71bafd70acbb by wenzelm:
avoid waste of resources due to dynamic simpset (amending 45c09620f726);
The file was modified src/HOL/Tools/record.ML (diff)
Changeset 74594:2f28a0a758ab by Norbert Schirmer _nschirmer@apple.com_:
fix latex
The file was modified src/HOL/Statespace/StateSpaceEx.thy (diff)
Changeset 74593:66f10c877542 by wenzelm:
clarified modules;
The file was addedsrc/Pure/ML/ml_instantiate.ML
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
Changeset 74592:3c587b7c3d5c by haftmann:
more generic bit/word lemmas for distribution
The file was modified src/HOL/Bit_Operations.thy (diff)
The file was modified src/HOL/Codegenerator_Test/Generate_Target_Nat.thy (diff)
The file was modified src/HOL/Euclidean_Division.thy (diff)
The file was modified src/HOL/Library/Code_Abstract_Nat.thy (diff)
The file was modified src/HOL/Library/Signed_Division.thy (diff)
The file was modified src/HOL/Library/Word.thy (diff)
The file was modified src/HOL/Num.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 74591:a0ab0dc28d3c by paulson:
merged
Changeset 74590:00ffae972fc0 by paulson _lp15@cam.ac.uk_:
Added / moved some simple set-theoretic lemmas
The file was modified src/HOL/Equiv_Relations.thy (diff)
The file was modified src/HOL/Library/Disjoint_Sets.thy (diff)
The file was modified src/HOL/Set.thy (diff)
Changeset 74589:ee92a47b47cb by wenzelm:
more CONTRIBUTORS and NEWS;
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
Changeset 74588:3cc363e8bfb2 by Norbert Schirmer _nschirmer@apple.com_:
cleanup; add Apple reference
The file was modified src/HOL/Statespace/StateSpaceEx.thy (diff)
The file was modified src/HOL/Statespace/distinct_tree_prover.ML (diff)
The file was modified src/HOL/Statespace/state_fun.ML (diff)
The file was modified src/HOL/Statespace/state_space.ML (diff)
Changeset 74587:ebb0b15c66e1 by Norbert Schirmer _nschirmer@apple.com_:
refine interface
The file was modified src/HOL/Statespace/distinct_tree_prover.ML (diff)
Changeset 74586:5ac762b53119 by Norbert Schirmer _nschirmer@apple.com_:
generalized component lookup for syntax and distinctness proofs. added some tracing.
The file was modified src/HOL/Statespace/StateSpaceEx.thy (diff)
The file was modified src/HOL/Statespace/state_fun.ML (diff)
The file was modified src/HOL/Statespace/state_space.ML (diff)