--- 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"
--- a/src/Pure/Pure.thy Sun Feb 25 19:19:11 2018 +0100
+++ b/src/Pure/Pure.thy Sun Feb 25 19:30:55 2018 +0100
@@ -94,15 +94,9 @@
and "named_theorems" :: thy_decl
abbrevs "===>" = "===>" (*prevent replacement of very long arrows*)
and "--->" = "\<midarrow>\<rightarrow>"
- and "default_sort" = ""
- and "simproc_setup" = ""
- and "hence" = ""
+ and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = ""
and "hence" = "then have"
- and "thus" = ""
and "thus" = "then show"
- and "apply_end" = ""
- and "realizers" = ""
- and "realizability" = ""
begin
section \<open>Isar commands\<close>