changeset 56361 | 9f9f60f4dbbf |
parent 53433 | 3b356b7f7cad |
child 63432 | ba7901e94e7b |
56360:1d122af2b11a | 56361:9f9f60f4dbbf |
---|---|
2 Author: Lars Noschinski |
2 Author: Lars Noschinski |
3 *) |
3 *) |
4 |
4 |
5 theory Simps_Case_Conv |
5 theory Simps_Case_Conv |
6 imports Main |
6 imports Main |
7 keywords "simps_of_case" "case_of_simps" :: thy_decl |
7 keywords "simps_of_case" :: thy_decl == "" and "case_of_simps" :: thy_decl |
8 begin |
8 begin |
9 |
9 |
10 ML_file "simps_case_conv.ML" |
10 ML_file "simps_case_conv.ML" |
11 |
11 |
12 end |
12 end |