tuned;
authorwenzelm
Sun Feb 25 19:30:55 2018 +0100 (24 months ago)
changeset 6772463e305429f8a
parent 67723 d11c5af083a5
child 67725 e6cd1fd4eb19
tuned;
src/HOL/Library/Simps_Case_Conv.thy
src/Pure/Pure.thy
     1.1 --- a/src/HOL/Library/Simps_Case_Conv.thy	Sun Feb 25 19:19:11 2018 +0100
     1.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy	Sun Feb 25 19:30:55 2018 +0100
     1.3 @@ -5,8 +5,7 @@
     1.4  theory Simps_Case_Conv
     1.5  imports Main
     1.6    keywords "simps_of_case" "case_of_simps" :: thy_decl
     1.7 -  abbrevs "simps_of_case" = ""
     1.8 -    and "case_of_simps" = ""
     1.9 +  abbrevs "simps_of_case" "case_of_simps" = ""
    1.10  begin
    1.11  
    1.12  ML_file "simps_case_conv.ML"
     2.1 --- a/src/Pure/Pure.thy	Sun Feb 25 19:19:11 2018 +0100
     2.2 +++ b/src/Pure/Pure.thy	Sun Feb 25 19:30:55 2018 +0100
     2.3 @@ -94,15 +94,9 @@
     2.4    and "named_theorems" :: thy_decl
     2.5  abbrevs "===>" = "===>"  (*prevent replacement of very long arrows*)
     2.6    and "--->" = "\<midarrow>\<rightarrow>"
     2.7 -  and "default_sort" = ""
     2.8 -  and "simproc_setup" = ""
     2.9 -  and "hence" = ""
    2.10 +  and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = ""
    2.11    and "hence" = "then have"
    2.12 -  and "thus" = ""
    2.13    and "thus" = "then show"
    2.14 -  and "apply_end" = ""
    2.15 -  and "realizers" = ""
    2.16 -  and "realizability" = ""
    2.17  begin
    2.18  
    2.19  section \<open>Isar commands\<close>