changeset 67724 | 63e305429f8a |
parent 67013 | 335a7dce7cb3 |
child 69568 | de09a7261120 |
--- a/src/HOL/Library/Simps_Case_Conv.thy Sun Feb 25 19:19:11 2018 +0100 +++ b/src/HOL/Library/Simps_Case_Conv.thy Sun Feb 25 19:30:55 2018 +0100 @@ -5,8 +5,7 @@ theory Simps_Case_Conv imports Main keywords "simps_of_case" "case_of_simps" :: thy_decl - abbrevs "simps_of_case" = "" - and "case_of_simps" = "" + abbrevs "simps_of_case" "case_of_simps" = "" begin ML_file "simps_case_conv.ML"