Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. export plain infix syntax;
  2. unused;
  3. merged
  4. more lemmas
  5. tuned
  6. more traditional formulation
Changeset 69003:a015f1d3ba0c by wenzelm:
export plain infix syntax;
The file was modified src/Pure/Syntax/syntax.ML (diff)
The file was modified src/Pure/Syntax/syntax_ext.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 69002:f0d4b1db0ea0 by wenzelm:
unused;
The file was modified src/Pure/Syntax/parser.ML (diff)
The file was modified src/Pure/Syntax/syntax.ML (diff)
Changeset 69001:f108b3b67ada by paulson:
merged
Changeset 69000:7cb3ddd60fd6 by paulson _lp15@cam.ac.uk_:
more lemmas
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Library/FuncSet.thy (diff)
The file was modified src/HOL/Zorn.thy (diff)
Changeset 68999:2af022252782 by nipkow:
tuned
The file was modified src/HOL/Library/Tree.thy (diff)
Changeset 68998:818898556504 by nipkow:
more traditional formulation
The file was modified src/HOL/Data_Structures/RBT_Set.thy (diff)
The file was modified src/HOL/Data_Structures/Tree2.thy (diff)
The file was modified src/HOL/Library/Tree.thy (diff)
The file was modified src/HOL/Library/Tree_Real.thy (diff)