Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified aliases (no warning for duplicates);
  2. eliminated pointless alias (no warning for duplicates);
  3. avoid warnings on duplicate rules in the given list;
  4. avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;
Changeset 63223:bcf4828bb125 by wenzelm:
clarified aliases (no warning for duplicates);
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML (diff)
Changeset 63222:fe92356ade42 by wenzelm:
eliminated pointless alias (no warning for duplicates);
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_util.ML (diff)
Changeset 63221:7d43fbbaba28 by wenzelm:
avoid warnings on duplicate rules in the given list;
The file was modified src/Pure/Isar/local_defs.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
Changeset 63220:06cbfbaf39c5 by wenzelm:
avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;
The file was modified src/Pure/ML_Bootstrap.thy (diff)