Summary
- more theorems
- sorted out some duplicate fact bindings
- more direct bootstrap of char type, still retaining the nibble representation for syntax
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) |
The file was modified | src/HOL/Nat.thy (diff) |
The file was modified | src/HOL/Tools/nat_arith.ML (diff) |
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) |