Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. NEWS;
  2. isabelle update_cartouches -t;
  3. update ROOT files as well: treated like .thy in Isabelle/jEdit;
  4. clarified isabelle_fonts license, to be used when the component is updated next time;
  5. tuned whitespace;
  6. clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
  7. always insist in specified resolver/compiler version;
  8. proper ML expressions, without trailing semicolons;
  9. insist in specified resolver/compiler version;
  10. simplified -- according to regular "ghci" script;
  11. clarified ML positions (see also 1a52baa70aed);
  12. more standard Resources.provide_parse_files: avoid duplicate markup reports;
  13. more uniform (see 1722cc56d22e);
  14. removed relics of ASCII syntax for indexed big operators
Changeset 69273:e86d8cb40610 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 69272:15e9ed5b28fb by wenzelm:
isabelle update_cartouches -t;
The file was modified src/Benchmarks/ROOT (diff)
The file was modified src/CCL/ROOT (diff)
The file was modified src/CTT/ROOT (diff)
The file was modified src/Cube/ROOT (diff)
The file was modified src/FOL/ROOT (diff)
The file was modified src/FOLP/ROOT (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Ring.thy (diff)
The file was modified src/HOL/Algebra/Sylow.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Eisbach/Eisbach.thy (diff)
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/Library/Code_Lazy.thy (diff)
The file was modified src/HOL/Library/IArray.thy (diff)
The file was modified src/HOL/Library/Landau_Symbols.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/String.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
The file was modified src/LCF/ROOT (diff)
The file was modified src/Pure/ROOT (diff)
The file was modified src/Sequents/ROOT (diff)
The file was modified src/ZF/ROOT (diff)
Changeset 69271:4cb70e7e36b9 by wenzelm:
update ROOT files as well: treated like .thy in Isabelle/jEdit;
The file was modified src/Pure/Tools/update_cartouches.scala (diff)
Changeset 69270:15463f546ee0 by wenzelm:
clarified isabelle_fonts license, to be used when the component is updated next time;
The file was modified lib/fonts/README (diff)
Changeset 69269:1bee990d443c by wenzelm:
tuned whitespace;
The file was modified NEWS (diff)
Changeset 69268:c1a27fce2076 by wenzelm:
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
The file was addedlib/scripts/ghc
The file was addedlib/scripts/ocaml
The file was addedlib/scripts/ocamlc
The file was modified NEWS (diff)
The file was modified lib/scripts/getsettings (diff)
The file was removedlib/Tools/ghc
The file was removedlib/Tools/ghci
The file was removedlib/Tools/ocaml
The file was removedlib/Tools/ocamlc
Changeset 69267:517655a528fe by wenzelm:
always insist in specified resolver/compiler version;
The file was modified lib/Tools/ghc (diff)
The file was modified lib/Tools/ghc_setup (diff)
The file was modified lib/scripts/getfunctions (diff)
Changeset 69266:7cc2d66a92a6 by wenzelm:
proper ML expressions, without trailing semicolons;
The file was modified src/HOL/Decision_Procs/Cooper.thy (diff)
The file was modified src/HOL/Decision_Procs/Ferrack.thy (diff)
The file was modified src/HOL/Decision_Procs/MIR.thy (diff)
Changeset 69265:bd215c56cd96 by wenzelm:
insist in specified resolver/compiler version;
The file was modified lib/Tools/ghc (diff)
Changeset 69264:021ea2abf42d by wenzelm:
simplified -- according to regular "ghci" script;
The file was modified lib/Tools/ghci (diff)
Changeset 69263:c546e37f6cb9 by wenzelm:
clarified ML positions (see also 1a52baa70aed);
The file was modified src/Pure/Isar/isar_cmd.ML (diff)
Changeset 69262:f94726501b37 by wenzelm:
more standard Resources.provide_parse_files: avoid duplicate markup reports;
The file was modified src/Pure/Pure.thy (diff)
Changeset 69261:a41f49148525 by wenzelm:
more uniform (see 1722cc56d22e);
The file was modified lib/Tools/ocaml (diff)
The file was modified lib/Tools/ocamlc (diff)
Changeset 69260:0a9688695a1b by haftmann:
removed relics of ASCII syntax for indexed big operators
The file was modified src/HOL/Analysis/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Continuous_Function.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Caratheodory.thy (diff)
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Embed_Measure.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Finite_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Measurable.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
The file was modified src/HOL/Analysis/Radon_Nikodym.thy (diff)
The file was modified src/HOL/Analysis/Regularity.thy (diff)
The file was modified src/HOL/Analysis/Riemann_Mapping.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Complex.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/IMP/Collecting.thy (diff)
The file was modified src/HOL/Library/Countable_Complete_Lattices.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Finite_Lattice.thy (diff)
The file was modified src/HOL/Library/Liminf_Limsup.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Product_Order.thy (diff)
The file was modified src/HOL/Probability/Discrete_Topology.thy (diff)
The file was modified src/HOL/Probability/Distribution_Functions.thy (diff)
The file was modified src/HOL/Probability/Essential_Supremum.thy (diff)
The file was modified src/HOL/Probability/Fin_Map.thy (diff)
The file was modified src/HOL/Probability/Giry_Monad.thy (diff)
The file was modified src/HOL/Probability/Helly_Selection.thy (diff)
The file was modified src/HOL/Probability/Projective_Family.thy (diff)
The file was modified src/HOL/Probability/Projective_Limit.thy (diff)
The file was modified src/HOL/Probability/SPMF.thy (diff)
The file was modified src/HOL/Probability/Stream_Space.thy (diff)
The file was modified src/HOL/Probability/Weak_Convergence.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)