Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. tuned;
  3. tuned signature -- prover-independence is presently theoretical;
  4. tuned;
  5. avoid confusion with 'case' and "cases";
  6. tuned;
  7. clarified: 'imports' is de-facto mandatory;
  8. support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
  9. tuned;
Changeset 63586:71ee1b8067cc by wenzelm:
merged
Changeset 63585:f4a308fdf664 by wenzelm:
tuned;
The file was modified src/HOL/Isar_Examples/Basic_Logic.thy (diff)
The file was modified src/HOL/Isar_Examples/Cantor.thy (diff)
The file was modified src/HOL/Isar_Examples/Drinker.thy (diff)
The file was modified src/HOL/Isar_Examples/Expr_Compiler.thy (diff)
The file was modified src/HOL/Isar_Examples/Fibonacci.thy (diff)
The file was modified src/HOL/Isar_Examples/First_Order_Logic.thy (diff)
The file was modified src/HOL/Isar_Examples/Group.thy (diff)
The file was modified src/HOL/Isar_Examples/Group_Context.thy (diff)
The file was modified src/HOL/Isar_Examples/Group_Notepad.thy (diff)
The file was modified src/HOL/Isar_Examples/Higher_Order_Logic.thy (diff)
The file was modified src/HOL/Isar_Examples/Hoare.thy (diff)
The file was modified src/HOL/Isar_Examples/Hoare_Ex.thy (diff)
The file was modified src/HOL/Isar_Examples/Peirce.thy (diff)
Changeset 63584:68751fe1c036 by wenzelm:
tuned signature -- prover-independence is presently theoretical;
The file was modified src/Pure/Isar/outer_syntax.scala (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/prover.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/Thy/thy_info.scala (diff)
The file was modified src/Pure/Thy/thy_syntax.scala (diff)
Changeset 63583:a39baba12732 by wenzelm:
tuned;
The file was modified src/HOL/Isar_Examples/Knaster_Tarski.thy (diff)
The file was modified src/HOL/Isar_Examples/Mutilated_Checkerboard.thy (diff)
The file was modified src/HOL/Isar_Examples/Puzzle.thy (diff)
The file was modified src/HOL/Isar_Examples/Schroeder_Bernstein.thy (diff)
The file was modified src/HOL/Isar_Examples/Structured_Statements.thy (diff)
The file was modified src/HOL/Isar_Examples/Summation.thy (diff)
Changeset 63582:161c5d8ae266 by wenzelm:
avoid confusion with 'case' and "cases";
The file was modified src/HOL/Library/Simps_Case_Conv.thy (diff)
Changeset 63581:a1bdc546f276 by wenzelm:
tuned;
The file was modified NEWS (diff)
Changeset 63580:7f06347a5013 by wenzelm:
clarified: 'imports' is de-facto mandatory;
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
Changeset 63579:73939a9b70a3 by wenzelm:
support &#039;abbrevs&#039; within theory header;<br>simplified &#039;keywords&#039;: no abbreviations here;
The file was modified NEWS (diff)
The file was modified etc/abbrevs (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/HOL/Library/Simps_Case_Conv.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HLim.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HSEQ.thy (diff)
The file was modified src/Pure/General/completion.scala (diff)
The file was modified src/Pure/General/multi_map.scala (diff)
The file was modified src/Pure/General/scan.scala (diff)
The file was modified src/Pure/Isar/keyword.scala (diff)
The file was modified src/Pure/Isar/outer_syntax.scala (diff)
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/PIDE/prover.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
The file was modified src/Pure/Thy/thy_info.scala (diff)
The file was modified src/Pure/Thy/thy_syntax.scala (diff)
Changeset 63578:e8990d0e3965 by wenzelm:
tuned;
The file was modified src/Pure/General/completion.scala (diff)