Skip to content
Failed

Changes

Summary

  1. merged
  2. more specific keyword kinds;
  3. tuned whitespace;
  4. include zarith in the default opam setup
  5. dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
  6. proper theory for type of dual ordered lattice in distribution
  7. slightly more complete check of code generation for immutable arrays
Changeset 69914:72301e1457b9 by wenzelm:
merged
Changeset 69913:ca515cf61651 by wenzelm:
more specific keyword kinds;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/HOL/BNF_Composition.thy (diff)
The file was modified src/HOL/BNF_Def.thy (diff)
The file was modified src/HOL/BNF_Greatest_Fixpoint.thy (diff)
The file was modified src/HOL/BNF_Least_Fixpoint.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Fun_Def.thy (diff)
The file was modified src/HOL/HOLCF/Cpodef.thy (diff)
The file was modified src/HOL/HOLCF/Domain.thy (diff)
The file was modified src/HOL/HOLCF/Fixrec.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Inductive.thy (diff)
The file was modified src/HOL/Library/BNF_Corec.thy (diff)
The file was modified src/HOL/Library/Datatype_Records.thy (diff)
The file was modified src/HOL/Library/Old_Recdef.thy (diff)
The file was modified src/HOL/Lifting.thy (diff)
The file was modified src/HOL/Nominal/Nominal.thy (diff)
The file was modified src/HOL/Partial_Function.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
The file was modified src/HOL/Quotient.thy (diff)
The file was modified src/HOL/Record.thy (diff)
The file was modified src/HOL/Statespace/StateSpaceLocale.thy (diff)
The file was modified src/HOL/Typedef.thy (diff)
The file was modified src/Pure/Isar/keyword.ML (diff)
The file was modified src/Pure/Isar/keyword.scala (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 69912:dd55d2c926d9 by wenzelm:
tuned whitespace;
The file was modified src/HOL/Types_To_Sets/Examples/Prerequisites.thy (diff)
Changeset 69911:036037573080 by haftmann:
include zarith in the default opam setup
The file was modified NEWS (diff)
The file was modified lib/Tools/ocaml_setup (diff)
Changeset 69910:0c0f7b4a72bf by haftmann:
dedicated environment setting for ocaml environment: ISABELLE_OPAM_ROOT is always present even if no envionrment is available
The file was modified lib/scripts/getsettings (diff)
The file was modified src/Tools/Code/code_ml.ML (diff)
Changeset 69909:5382f5691a11 by haftmann:
proper theory for type of dual ordered lattice in distribution
The file was addedsrc/HOL/Library/Dual_Ordered_Lattice.thy
The file was modified src/HOL/Library/Library.thy (diff)
Changeset 69908:1bd74a0944b3 by haftmann:
slightly more complete check of code generation for immutable arrays
The file was modified src/HOL/ex/IArray_Examples.thy (diff)