Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
  2. more symbols;
  3. misc tuning and modernization;
  4. implicit keyword completion only for actual words (amending 73939a9b70a3);
Changeset 63590:4854f7ee0987 by wenzelm:
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
The file was modified lib/texinputs/isabelle.sty (diff)
The file was modified src/HOL/Nonstandard_Analysis/document/root.tex (diff)
The file was modified src/Pure/Thy/latex.ML (diff)
Changeset 63589:58aab4745e85 by wenzelm:
more symbols;
The file was modified src/HOL/Library/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Library/Fundamental_Theorem_Algebra.thy (diff)
The file was modified src/HOL/Library/Inner_Product.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSComplex.thy (diff)
The file was modified src/HOL/Probability/Characteristic_Functions.thy (diff)
The file was modified src/HOL/Probability/Levy.thy (diff)
The file was modified src/HOL/ex/BinEx.thy (diff)
The file was modified src/HOL/ex/Cubic_Quartic.thy (diff)
Changeset 63588:d0e2bad67bd4 by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Groups.thy (diff)
The file was modified src/HOL/Inductive.thy (diff)
The file was modified src/HOL/Lattices.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
The file was modified src/HOL/Set.thy (diff)
Changeset 63587:881e8e2cfec2 by wenzelm:
implicit keyword completion only for actual words (amending 73939a9b70a3);
The file was modified src/Pure/General/completion.scala (diff)
The file was modified src/Pure/Isar/outer_syntax.scala (diff)