equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Simps_Case_Conv.thy |
1 (* Title: HOL/Library/Simps_Case_Conv.thy |
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 Case_Converter |
7 keywords "simps_of_case" "case_of_simps" :: thy_decl |
7 keywords "simps_of_case" "case_of_simps" :: thy_decl |
8 abbrevs "simps_of_case" "case_of_simps" = "" |
8 abbrevs "simps_of_case" "case_of_simps" = "" |
9 begin |
9 begin |
10 |
10 |
11 ML_file "simps_case_conv.ML" |
11 ML_file "simps_case_conv.ML" |