Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. 'code_reflect' only supports new-style 'file_prefix'; avoid fragile file "$ISABELLE_TMP/rat.ML";
  2. tuned signature -- more exports;
  3. tuned signature;
  4. A few results in Algebra, and bits for Analysis
Changeset 70022:49e178cbf923 by wenzelm:
&#039;code_reflect&#039; only supports new-style &#039;file_prefix&#039;;<br>avoid fragile file &quot;$ISABELLE_TMP/rat.ML&quot;;
The file was modified NEWS (diff)
The file was modified src/Doc/Codegen/Further.thy (diff)
The file was modified src/Doc/Isar_Ref/HOL_Specific.thy (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 70021:e6e634836556 by wenzelm:
tuned signature -- more exports;
The file was modified src/Tools/Code/code_target.ML (diff)
Changeset 70020:0cb334eee651 by wenzelm:
tuned signature;
The file was modified src/Pure/General/path.ML (diff)
Changeset 70019:095dce9892e8 by paulson _lp15@cam.ac.uk_:
A few results in Algebra, and bits for Analysis
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Generated_Groups.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Polynomials.thy (diff)
The file was modified src/HOL/Algebra/RingHom.thy (diff)
The file was modified src/HOL/Algebra/Zassenhaus.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Limits.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/T1_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Vector_Spaces.thy (diff)