changeset 63582 | 161c5d8ae266 |
parent 63579 | 73939a9b70a3 |
child 67013 | 335a7dce7cb3 |
63581:a1bdc546f276 | 63582:161c5d8ae266 |
---|---|
6 imports Main |
6 imports Main |
7 keywords |
7 keywords |
8 "simps_of_case" "case_of_simps" :: thy_decl |
8 "simps_of_case" "case_of_simps" :: thy_decl |
9 abbrevs |
9 abbrevs |
10 "simps_of_case" = "" |
10 "simps_of_case" = "" |
11 "case_of_simps" = "" |
|
11 begin |
12 begin |
12 |
13 |
13 ML_file "simps_case_conv.ML" |
14 ML_file "simps_case_conv.ML" |
14 |
15 |
15 end |
16 end |