Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust: avoid implicit setup (with default resolver);
  2. more portable;
  3. proper path;
  4. tuned;
  5. merged
  6. avoid strict evaluation of "isabelle_stack path --programs";
  7. enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
  8. support for GHC via command-line tools;
  9. tuned;
  10. tuned message;
  11. auto update;
  12. isabelle_stack as portable shell function;
  13. tuned;
  14. added Array files
  15. new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
  16. more intuitive and simpler (but slower) proofs
Changeset 69158:1722cc56d22e by wenzelm:
more robust: avoid implicit setup (with default resolver);
The file was modified lib/Tools/ghc (diff)
The file was modified lib/Tools/ghci (diff)
Changeset 69157:22ae1d926f96 by wenzelm:
more portable;
The file was modified lib/scripts/getfunctions (diff)
The file was modified lib/scripts/getsettings (diff)
Changeset 69156:e8ef77b7e1a0 by wenzelm:
proper path;
The file was modified lib/scripts/getsettings (diff)
Changeset 69155:12ff5e476752 by wenzelm:
tuned;
The file was modified NEWS (diff)
Changeset 69154:9d70340b565c by wenzelm:
merged
Changeset 69153:108beabc1bc6 by wenzelm:
avoid strict evaluation of "isabelle_stack path --programs";
The file was modified lib/scripts/getsettings (diff)
Changeset 69152:77eede3f40e2 by wenzelm:
enforce settings that are likely to be outdated, e.g. in $ISABELLE_HOME_USER/etc/settings;
The file was modified lib/scripts/getsettings (diff)
Changeset 69151:b310bc57f55f by wenzelm:
support for GHC via command-line tools;
The file was addedlib/Tools/ghc
The file was addedlib/Tools/ghc_setup
The file was addedlib/Tools/ghc_stack
The file was addedlib/Tools/ghci
The file was modified NEWS (diff)
The file was modified etc/settings (diff)
The file was modified lib/scripts/getsettings (diff)
Changeset 69150:545b68843709 by wenzelm:
tuned;
The file was modified lib/scripts/getfunctions (diff)
Changeset 69149:8c501c406d24 by wenzelm:
tuned message;
The file was modified lib/Tools/ocaml_setup (diff)
Changeset 69148:d0517da45e5c by wenzelm:
auto update;
The file was modified Admin/components/components.sha1 (diff)
Changeset 69147:6f4d561ea621 by wenzelm:
isabelle_stack as portable shell function;
The file was addedAdmin/haskell/stack/README
The file was addedAdmin/haskell/stack/settings
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified etc/settings (diff)
The file was modified lib/scripts/getfunctions (diff)
Changeset 69146:0b0680016187 by wenzelm:
tuned;
The file was modified Admin/components/main (diff)
Changeset 69145:806be481aa57 by nipkow:
added Array files
The file was addedsrc/HOL/Data_Structures/Array_Braun.thy
The file was addedsrc/HOL/Data_Structures/Array_Specs.thy
The file was modified src/HOL/ROOT (diff)
Changeset 69144:f13b82281715 by paulson _lp15@cam.ac.uk_:
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
The file was addedsrc/HOL/Analysis/Abstract_Topology.thy
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Library/FuncSet.thy (diff)
The file was modified src/HOL/Meson.thy (diff)
The file was modified src/HOL/Metis_Examples/Tarski.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/UNITY/ProgressSets.thy (diff)
Changeset 69143:5acb1eece41b by nipkow:
more intuitive and simpler (but slower) proofs
The file was modified src/HOL/Data_Structures/Braun_Tree.thy (diff)