Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. clarified document antiquotation @{theory};
  3. include target sessions as well: avoid default "Draft" qualification;
  4. clarified signature;
  5. more uniform syntax;
  6. more documentation;
  7. merged
  8. de-applying Divisibility
Changeset 68485:28f9e9b80c49 by wenzelm:
merged
Changeset 68484:59793df7f853 by wenzelm:
clarified document antiquotation @{theory};
The file was modified NEWS (diff)
The file was modified src/Doc/Codegen/Adaptation.thy (diff)
The file was modified src/Doc/Codegen/Foundations.thy (diff)
The file was modified src/Doc/Codegen/Further.thy (diff)
The file was modified src/Doc/Codegen/Introduction.thy (diff)
The file was modified src/Doc/Codegen/Refinement.thy (diff)
The file was modified src/Doc/Datatypes/Datatypes.thy (diff)
The file was modified src/Doc/Eisbach/Manual.thy (diff)
The file was modified src/Doc/Eisbach/Preface.thy (diff)
The file was modified src/Doc/Isar_Ref/Document_Preparation.thy (diff)
The file was modified src/Doc/Isar_Ref/HOL_Specific.thy (diff)
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Tutorial/Types/Axioms.thy (diff)
The file was modified src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy (diff)
The file was modified src/HOL/Algebra/AbelCoset.thy (diff)
The file was modified src/HOL/Algebra/Sylow.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Codegenerator_Test/Candidates.thy (diff)
The file was modified src/HOL/Data_Structures/Set2_Join.thy (diff)
The file was modified src/HOL/Groebner_Basis.thy (diff)
The file was modified src/HOL/IMP/Abs_Int0.thy (diff)
The file was modified src/HOL/IMP/Compiler2.thy (diff)
The file was modified src/HOL/IMP/Live_True.thy (diff)
The file was modified src/HOL/Library/Code_Test.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/RBT_Mapping.thy (diff)
The file was modified src/HOL/Library/Tree_Multiset.thy (diff)
The file was modified src/HOL/Library/Tree_Real.thy (diff)
The file was modified src/HOL/Order_Relation.thy (diff)
The file was modified src/HOL/Quickcheck_Narrowing.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/ex/Erdoes_Szekeres.thy (diff)
The file was modified src/HOL/ex/Sum_of_Powers.thy (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/theory.ML (diff)
Changeset 68483:087d32a40129 by wenzelm:
include target sessions as well: avoid default "Draft" qualification;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 68482:cb84beb84ca9 by wenzelm:
clarified signature;
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
The file was modified src/Pure/Tools/thm_deps.ML (diff)
The file was modified src/Pure/Tools/thy_deps.ML (diff)
The file was modified src/Pure/context.ML (diff)
The file was modified src/Pure/theory.ML (diff)
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 68481:fb6afa538b04 by wenzelm:
more uniform syntax;
The file was modified src/Doc/Isar_Ref/Document_Preparation.thy (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
Changeset 68480:27be5b4cb80d by wenzelm:
more documentation;
The file was modified src/Doc/Eisbach/Preface.thy (diff)
Changeset 68479:f839ce4af873 by paulson:
merged
Changeset 68478:f75a7d2be8c5 by paulson _lp15@cam.ac.uk_:
de-applying Divisibility
The file was modified src/HOL/Algebra/Divisibility.thy (diff)