Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. prefer symbols;
  3. tuned;
  4. more abbrevs;
  5. allow multiple entries of and_list (on both sides);
  6. eliminated ASCII syntax from Pure bootstrap; tuned comments;
  7. merged
  8. new material on matrices, etc., and consolidating duplicate results about of_nat
  9. notation for dummy sort;
Changeset 67726:0cd2fd0c2dcf by wenzelm:
merged
Changeset 67725:e6cd1fd4eb19 by wenzelm:
prefer symbols;
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/unify.ML (diff)
Changeset 67724:63e305429f8a by wenzelm:
tuned;
The file was modified src/HOL/Library/Simps_Case_Conv.thy (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 67723:d11c5af083a5 by wenzelm:
more abbrevs;
The file was modified src/HOL/Transitive_Closure.thy (diff)
Changeset 67722:012f1e8a1209 by wenzelm:
allow multiple entries of and_list (on both sides);
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
Changeset 67721:5348bea4accd by wenzelm:
eliminated ASCII syntax from Pure bootstrap;<br>tuned comments;
The file was modified src/Pure/Isar/local_defs.ML (diff)
The file was modified src/Pure/Isar/obtain.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/Isar/subgoal.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Syntax/simple_syntax.ML (diff)
The file was modified src/Pure/Tools/find_theorems.ML (diff)
The file was modified src/Pure/assumption.ML (diff)
The file was modified src/Pure/conjunction.ML (diff)
The file was modified src/Pure/conv.ML (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/goal.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/primitive_defs.ML (diff)
The file was modified src/Pure/pure_thy.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/tactic.ML (diff)
The file was modified src/Pure/term.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/unify.ML (diff)
The file was modified src/Pure/variable.ML (diff)
Changeset 67720:b342f96e47b5 by paulson:
merged
Changeset 67719:bffb7482faaa by paulson _lp15@cam.ac.uk_:
new material on matrices, etc., and consolidating duplicate results about of_nat
The file was modified src/HOL/Analysis/Ball_Volume.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Great_Picard.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
Changeset 67718:17874d43d3b3 by wenzelm:
notation for dummy sort;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Pure/Syntax/syntax_phases.ML (diff)
The file was modified src/Pure/pure_thy.ML (diff)