Summary
- Tidied several ugly proofs in some elderly examples
The file was modified | src/HOL/Induct/QuoDataType.thy (diff) |
The file was modified | src/HOL/Induct/QuoNestedDataType.thy (diff) |
The file was modified | src/HOL/Induct/QuoDataType.thy (diff) |
The file was modified | src/HOL/Induct/QuoNestedDataType.thy (diff) |