Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. updated subtle side-conditions;
  3. some uses of 'obtain' with structure statement;
  4. 'obtain' supports structured statements (similar to 'define');
  5. more portable: GNU find no longer supports "-perm +mode";
  6. more uniform operations for structured statements;
  7. defs are closed, which leads to proper auto_bind_facts; misc tuning;
  8. tuned notation;
  9. misc tuning and modernization;
Changeset 63062:60406bf310f8 by wenzelm:
merged
Changeset 63061:21ebc2f5c571 by wenzelm:
updated subtle side-conditions;
The file was modified Admin/Release/CHECKLIST (diff)
Changeset 63060:293ede07b775 by wenzelm:
some uses of 'obtain' with structure statement;
The file was modified src/HOL/Library/ContNotDenum.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Fun_Lexorder.thy (diff)
The file was modified src/HOL/Library/FuncSet.thy (diff)
The file was modified src/HOL/Library/Function_Growth.thy (diff)
The file was modified src/HOL/Library/Fundamental_Theorem_Algebra.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
The file was modified src/HOL/Library/Ramsey.thy (diff)
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
The file was modified src/HOL/Proofs/Lambda/WeakNorm.thy (diff)
The file was modified src/HOL/ex/Gauge_Integration.thy (diff)
Changeset 63059:3f577308551e by wenzelm:
'obtain' supports structured statements (similar to 'define');
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Proof.thy (diff)
The file was modified src/Pure/Isar/obtain.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 63058:8804faa80bc9 by wenzelm:
more portable: GNU find no longer supports "-perm +mode";
The file was modified Admin/lib/Tools/makedist (diff)
The file was modified Admin/lib/Tools/makedist_bundle (diff)
Changeset 63057:50802acac277 by wenzelm:
more uniform operations for structured statements;
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/proof_context.ML (diff)
Changeset 63056:9b95ae9ec671 by wenzelm:
defs are closed, which leads to proper auto_bind_facts;<br>misc tuning;
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/proof_context.ML (diff)
The file was modified src/Pure/logic.ML (diff)
Changeset 63055:ae0ca486bd3f by wenzelm:
tuned notation;
The file was modified src/HOL/ex/CTL.thy (diff)
The file was modified src/HOL/ex/document/root.tex (diff)
Changeset 63054:1b237d147cc4 by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/ex/Abstract_NAT.thy (diff)
The file was modified src/HOL/ex/CTL.thy (diff)
The file was modified src/HOL/ex/Cartouche_Examples.thy (diff)
The file was modified src/HOL/ex/Coherent.thy (diff)
The file was modified src/HOL/ex/Cubic_Quartic.thy (diff)