Skip to content
Success

Changes

Summary

  1. merged
  2. proper \usepackage[T1]{fontenc};
  3. more robust init: avoid spilling opam artifacts;
  4. proper type-setting of cartouches (requires T1); \usepackage[T1]{fontenc} is default for mkroot; \usepackage[utf8]{inputenc} is obsolete in lualatex;
  5. provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04;
  6. more robust; eliminated perl;
  7. removed unused latex packages;
  8. obsolete (see 0c837beeb5e7);
  9. proper Isabelle/Scala tool --- avoid perl;
Changeset 73407:603010a9e611 by wenzelm:
merged
Changeset 73406:9939146b90ad by wenzelm:
proper \usepackage[T1]{fontenc};
The file was modified src/HOL/Bali/document/root.tex (diff)
The file was modified src/HOL/Hoare/document/root.tex (diff)
The file was modified src/HOL/Proofs/Lambda/document/root.tex (diff)
Changeset 73405:8510c6e98228 by wenzelm:
more robust init: avoid spilling opam artifacts;
The file was modified lib/Tools/ocaml_setup (diff)
Changeset 73404:299f6a8faccc by wenzelm:
proper type-setting of cartouches (requires T1);<br>\usepackage[T1]{fontenc} is default for mkroot;<br>\usepackage[utf8]{inputenc} is obsolete in lualatex;
The file was modified NEWS (diff)
The file was modified lib/texinputs/isabelle.sty (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)
The file was modified src/CTT/document/root.tex (diff)
The file was modified src/Doc/Functions/document/root.tex (diff)
The file was modified src/FOL/document/root.tex (diff)
The file was modified src/FOL/ex/document/root.tex (diff)
The file was modified src/HOL/Algebra/document/root.tex (diff)
The file was modified src/HOL/Analysis/document/root.tex (diff)
The file was modified src/HOL/Auth/document/root.tex (diff)
The file was modified src/HOL/Cardinals/document/root.tex (diff)
The file was modified src/HOL/Complex_Analysis/document/root.tex (diff)
The file was modified src/HOL/Data_Structures/document/root.tex (diff)
The file was modified src/HOL/Examples/document/root.tex (diff)
The file was modified src/HOL/HOLCF/IMP/document/root.tex (diff)
The file was modified src/HOL/HOLCF/document/root.tex (diff)
The file was modified src/HOL/Hahn_Banach/document/root.tex (diff)
The file was modified src/HOL/Homology/document/root.tex (diff)
The file was modified src/HOL/IMP/document/root.tex (diff)
The file was modified src/HOL/Induct/document/root.tex (diff)
The file was modified src/HOL/Isar_Examples/document/root.tex (diff)
The file was modified src/HOL/Lattice/document/root.tex (diff)
The file was modified src/HOL/Library/document/root.tex (diff)
The file was modified src/HOL/Matrix_LP/document/root.tex (diff)
The file was modified src/HOL/MicroJava/document/root.tex (diff)
The file was modified src/HOL/NanoJava/document/root.tex (diff)
The file was modified src/HOL/Nonstandard_Analysis/document/root.tex (diff)
The file was modified src/HOL/Number_Theory/document/root.tex (diff)
The file was modified src/HOL/Probability/document/root.tex (diff)
The file was modified src/HOL/Proofs/Extraction/document/root.tex (diff)
The file was modified src/HOL/Real_Asymp/Manual/document/root.tex (diff)
The file was modified src/HOL/SET_Protocol/document/root.tex (diff)
The file was modified src/HOL/SPARK/Manual/document/root.tex (diff)
The file was modified src/HOL/Statespace/document/root.tex (diff)
The file was modified src/HOL/UNITY/document/root.tex (diff)
The file was modified src/HOL/Unix/document/root.tex (diff)
The file was modified src/HOL/document/root.tex (diff)
The file was modified src/Pure/Examples/document/root.tex (diff)
The file was modified src/Pure/Tools/mkroot.scala (diff)
The file was modified src/ZF/AC/document/root.tex (diff)
The file was modified src/ZF/Constructible/document/root.tex (diff)
The file was modified src/ZF/IMP/document/root.tex (diff)
The file was modified src/ZF/Induct/document/root.tex (diff)
The file was modified src/ZF/document/root.tex (diff)
Changeset 73403:e19cb4c11409 by wenzelm:
provide \usepackage{textcomp} (again), for the sake of Ubuntu 16.04;
The file was modified src/Doc/Isar_Ref/document/root.tex (diff)
Changeset 73402:7eecb5231f61 by wenzelm:
more robust;<br>eliminated perl;
The file was modified lib/Tools/components (diff)
Changeset 73401:8b464825d2b5 by wenzelm:
removed unused latex packages;
The file was modified src/Doc/Classes/document/root.tex (diff)
The file was modified src/Doc/Codegen/document/root.tex (diff)
The file was modified src/Doc/Corec/document/root.tex (diff)
The file was modified src/Doc/Datatypes/document/root.tex (diff)
The file was modified src/Doc/Eisbach/document/root.tex (diff)
The file was modified src/Doc/Functions/document/root.tex (diff)
The file was modified src/Doc/Implementation/document/root.tex (diff)
The file was modified src/Doc/Isar_Ref/document/root.tex (diff)
The file was modified src/Doc/Tutorial/document/root.tex (diff)
Changeset 73400:e488f4bb1c79 by wenzelm:
obsolete (see 0c837beeb5e7);
The file was removedlib/scripts/timestart.bash
The file was removedlib/scripts/timestop.bash
Changeset 73399:48569c862eb8 by wenzelm:
proper Isabelle/Scala tool --- avoid perl;
The file was addedsrc/Pure/Tools/logo.scala
The file was modified src/Doc/System/Misc.thy (diff)
The file was modified src/Pure/System/isabelle_tool.scala (diff)
The file was modified src/Pure/build-jars (diff)
The file was removedlib/Tools/logo