Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged;
  2. updated to 146757999c8d;
  3. theory Pure is default presentation context;
  4. clarified implicit Pure.thy;
  5. prefer qualified names;
  6. tuned;
  7. check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
  8. more operations;
  9. tuned;
  10. clarified output (see also 909dcdec2122, 34d1913f0b20);
  11. more operations;
  12. tuned;
  13. moved in some material from Euler-MacLaurin
Changeset 67383:aacea75450b4 by wenzelm:
merged;
Changeset 67382:39e4668ded4f by wenzelm:
updated to 146757999c8d;
The file was modified src/HOL/ex/Cartouche_Examples.thy (diff)
Changeset 67381:146757999c8d by wenzelm:
theory Pure is default presentation context;
The file was modified NEWS (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/ML/ml_file.ML (diff)
The file was modified src/Pure/PIDE/command.ML (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/debugger.ML (diff)
The file was modified src/Pure/Tools/rail.ML (diff)
The file was modified src/Pure/pure_syn.ML (diff)
Changeset 67380:8bef51521f21 by wenzelm:
clarified implicit Pure.thy;
The file was modified src/Pure/ML/ml_pp.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/theory.ML (diff)
Changeset 67379:c2dfc510a38c by wenzelm:
prefer qualified names;
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_tactic.ML (diff)
The file was modified src/Provers/order.ML (diff)
The file was modified src/Provers/quasi.ML (diff)
The file was modified src/Provers/trancl.ML (diff)
Changeset 67378:2ebd0ef3a6b6 by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67377:143665524d8e by wenzelm:
check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
The file was modified src/Pure/ML/ml_file.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67376:d5007d93bcc6 by wenzelm:
more operations;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 67375:c0c36348a4fb by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67374:5a049cf98438 by wenzelm:
clarified output (see also 909dcdec2122, 34d1913f0b20);
The file was modified lib/texinputs/isabelle.sty (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67373:17f9fa98abab by wenzelm:
more operations;
The file was modified src/Pure/General/symbol.ML (diff)
Changeset 67372:820f3cbae27a by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 67371:2d9cf74943e1 by paulson _lp15@cam.ac.uk_:
moved in some material from Euler-MacLaurin
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Parity.thy (diff)