Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. generalized generation of coinduction goal (towards nonuniform codatatypes)
  2. export ML functions (towards nonuniform codatatypes) + signature tuning
  3. export ML function
  4. more uniform div/mod relations
  5. proper logical constants
  6. prefer existing logical constant over abbreviation
  7. dropped aliasses
  8. removed dangerous simp rule: prime computations can be excessively long
Changeset 64638:235df39ade87 by blanchet:
generalized generation of coinduction goal (towards nonuniform codatatypes)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
Changeset 64637:a15785625f7c by blanchet:
export ML functions (towards nonuniform codatatypes) + signature tuning
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.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_gfp_grec_sugar.ML (diff)
Changeset 64636:a42dbe9d2c1f by blanchet:
export ML function
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML (diff)
Changeset 64635:255741c5f862 by haftmann:
more uniform div/mod relations
The file was modified src/HOL/Divides.thy (diff)
The file was modified src/HOL/Library/Polynomial.thy (diff)
Changeset 64634:5bd30359e46e by haftmann:
proper logical constants
The file was modified NEWS (diff)
The file was modified src/HOL/Partial_Function.thy (diff)
The file was modified src/HOL/Probability/Probability_Mass_Function.thy (diff)
The file was modified src/HOL/Probability/SPMF.thy (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 64633:5ebcf6c525f1 by haftmann:
prefer existing logical constant over abbreviation
The file was modified NEWS (diff)
The file was modified src/HOL/Relation.thy (diff)
Changeset 64632:9df24b8b6c0a by haftmann:
dropped aliasses
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Transitive_Closure_Table.thy (diff)
The file was modified src/HOL/Relation.thy (diff)
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 64631:7705926ee595 by haftmann:
removed dangerous simp rule: prime computations can be excessively long
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)