Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust support for ARM64 platform;
  2. proper support for Apple Silicon (ARM64);
  3. merged
  4. tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;
  5. proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;
  6. proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;
  7. made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
  8. made tactic more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
Changeset 78493:1e80fc36776c by wenzelm:
more robust support for ARM64 platform;
The file was modified ANNOUNCE (diff)
Changeset 78492:aeda5a004d89 by wenzelm:
proper support for Apple Silicon (ARM64);
The file was modified src/Pure/Admin/build_history.scala (diff)
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 78491:c7bd8f8f7547 by wenzelm:
merged
Changeset 78490:9ea4135c8bef by wenzelm:
tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;
The file was modified src/Pure/PIDE/document.ML (diff)
Changeset 78489:40d50936484c by wenzelm:
proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;
The file was modified src/Pure/PIDE/document.ML (diff)
Changeset 78488:44ffc06187e0 by wenzelm:
proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 78487:da437a9f2823 by traytel:
made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML (diff)
Changeset 78486:e72f8009a4f0 by traytel:
made tactic more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)