Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. document that n2m does not depend on most things in fp_sugar in its type
  2. clarified rule structure;
  3. accomodate Isabelle identifiers with subscripts;
  4. more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
  5. eliminated unused argument (see also 58110c1e02bc);
  6. add le_log_of_power and le_log2_of_power by Tobias Nipkow
  7. unified CHAR with CHR syntax
Changeset 62684:cb20e8828196 by traytel:
document that n2m does not depend on most things in fp_sugar in its type
The file was modified src/HOL/Tools/BNF/bnf_comp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML (diff)
Changeset 62683:ddd1c864408b by wenzelm:
clarified rule structure;
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
Changeset 62682:0c9b1857504b by wenzelm:
accomodate Isabelle identifiers with subscripts;
The file was modified src/Tools/jEdit/src/modes/isabelle-ml.xml (diff)
The file was modified src/Tools/jEdit/src/modes/isabelle-news.xml (diff)
The file was modified src/Tools/jEdit/src/modes/isabelle-options.xml (diff)
The file was modified src/Tools/jEdit/src/modes/isabelle-root.xml (diff)
The file was modified src/Tools/jEdit/src/modes/isabelle.xml (diff)
Changeset 62681:45b8dd2d3827 by wenzelm:
more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
The file was modified src/Pure/Isar/element.ML (diff)
Changeset 62680:646b84666a56 by wenzelm:
eliminated unused argument (see also 58110c1e02bc);
The file was modified src/Pure/Isar/element.ML (diff)
The file was modified src/Pure/Isar/interpretation.ML (diff)
The file was modified src/Pure/Isar/isar_syn.ML (diff)
Changeset 62679:092cb9c96c99 by hoelzl:
add le_log_of_power and le_log2_of_power by Tobias Nipkow
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 62678:843ff6f1de38 by haftmann:
unified CHAR with CHR syntax
The file was modified NEWS (diff)
The file was modified src/HOL/String.thy (diff)