Skip to content
Failed

Changes

Summary

  1. more theorems
  2. sorted out some duplicate fact bindings
  3. more direct bootstrap of char type, still retaining the nibble representation for syntax
Changeset 62366:95c6cf433c91 by haftmann:
more theorems
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Number_Theory/Factorial_Ring.thy (diff)
The file was modified src/HOL/Power.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 62365:8a105c235b1f by haftmann:
sorted out some duplicate fact bindings
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Tools/nat_arith.ML (diff)
Changeset 62364:9209770bdcdf by haftmann:
more direct bootstrap of char type, still retaining the nibble representation for syntax
The file was modified src/HOL/Library/Code_Char.thy (diff)
The file was modified src/HOL/Quickcheck_Exhaustive.thy (diff)
The file was modified src/HOL/String.thy (diff)