Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. VSCode extension for official Isabelle release;
  2. merged
  3. clearout of some useless lemmas
  4. merged
  5. more bibtex fields;
  6. clarified PIDE markup;
  7. De-applying and combining lemmas to make structured proofs
  8. clarified directory location;
  9. more lemmas
  10. more correct simulation of eigen context for generated Isar statements
Changeset 70234:4e0834322981 by wenzelm:
VSCode extension for official Isabelle release;
The file was modified src/Tools/VSCode/extension/README.md (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 70233:778366b0f519 by paulson:
merged
Changeset 70232:d19266b7465f by paulson _lp15@cam.ac.uk_:
clearout of some useless lemmas
The file was modified src/HOL/Nonstandard_Analysis/HyperDef.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSA.thy (diff)
Changeset 70231:cdbc8d92c349 by wenzelm:
merged
Changeset 70230:8ba266889dee by wenzelm:
more bibtex fields;
The file was modified src/Pure/Thy/bibtex.scala (diff)
Changeset 70229:c03f381fd373 by wenzelm:
clarified PIDE markup;
The file was modified etc/options (diff)
The file was modified src/Pure/General/comment.ML (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
Changeset 70228:2d5b122aa0ff by paulson _lp15@cam.ac.uk_:
De-applying and combining lemmas to make structured proofs
The file was modified src/HOL/Nonstandard_Analysis/CLim.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/HOL/Nonstandard_Analysis/HSeries.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HTranscendental.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HyperNat.thy (diff)
Changeset 70227:ce9134bdc1d4 by wenzelm:
clarified directory location;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 70226:accbd801fefa by haftmann:
more lemmas
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Num.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
Changeset 70225:129757af1096 by haftmann:
more correct simulation of eigen context for generated Isar statements
The file was modified src/HOL/ex/Sketch_and_Explore.thy (diff)