| changeset 63579 | 73939a9b70a3 |
| parent 63432 | ba7901e94e7b |
| child 63582 | 161c5d8ae266 |
--- a/src/HOL/Library/Simps_Case_Conv.thy Tue Aug 02 11:49:30 2016 +0200 +++ b/src/HOL/Library/Simps_Case_Conv.thy Tue Aug 02 17:35:18 2016 +0200 @@ -5,8 +5,9 @@ theory Simps_Case_Conv imports Main keywords - "simps_of_case" :: thy_decl == "" and - "case_of_simps" :: thy_decl + "simps_of_case" "case_of_simps" :: thy_decl +abbrevs + "simps_of_case" = "" begin ML_file "simps_case_conv.ML"