renamed Goal constant to prop;
authorwenzelm
Fri Oct 28 22:27:51 2005 +0200 (2005-10-28 ago)
changeset 18024853e8219732a
parent 18023 3900037edf3d
child 18025 7dac6858168d
renamed Goal constant to prop;
src/HOL/Tools/meson.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Fri Oct 28 22:27:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Oct 28 22:27:51 2005 +0200
     1.3 @@ -233,7 +233,7 @@
     1.4        (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
     1.5        
     1.6  val has_meta_conn = 
     1.7 -    exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]);
     1.8 +    exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
     1.9    
    1.10  (*Raises an exception if any Vars in the theorem mention type bool; they
    1.11    could cause make_horn to loop! Also rejects functions whose arguments are 
     2.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 28 22:27:47 2005 +0200
     2.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 28 22:27:51 2005 +0200
     2.3 @@ -32,8 +32,8 @@
     2.4      val equal_elim_axm = ax equal_elim_axm [];
     2.5      val symmetric_axm = ax symmetric_axm [propT];
     2.6  
     2.7 -    fun rew' _ (PThm (("ProtoPure.goalD", _), _, _, _) % _ %%
     2.8 -        (PThm (("ProtoPure.goalI", _), _, _, _) % _ %% prf)) = SOME prf
     2.9 +    fun rew' _ (PThm (("ProtoPure.protectD", _), _, _, _) % _ %%
    2.10 +        (PThm (("ProtoPure.protectI", _), _, _, _) % _ %% prf)) = SOME prf
    2.11        | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
    2.12          (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
    2.13        | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    2.14 @@ -41,16 +41,16 @@
    2.15              SOME (equal_intr_axm % B % A %% prf2 %% prf1)
    2.16  
    2.17        | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    2.18 -        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
    2.19 +        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
    2.20            _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
    2.21 -        ((tg as PThm (("ProtoPure.goalI", _), _, _, _)) % _ %% prf2)) =
    2.22 +        ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) =
    2.23          SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    2.24  
    2.25        | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    2.26          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    2.27 -          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
    2.28 +          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
    2.29               _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
    2.30 -        ((tg as PThm (("ProtoPure.goalI", _), _, _, _)) % _ %% prf2)) =
    2.31 +        ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) =
    2.32          SOME (tg %> B %% (equal_elim_axm %> A %> B %%
    2.33            (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
    2.34  
     3.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Oct 28 22:27:47 2005 +0200
     3.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Oct 28 22:27:51 2005 +0200
     3.3 @@ -251,7 +251,7 @@
     3.4    ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000))];
     3.5  
     3.6  val pure_syntax_output =
     3.7 - [("Goal", "prop => prop", Mixfix ("_", [0], 0)),
     3.8 + [("prop", "prop => prop", Mixfix ("_", [0], 0)),
     3.9    ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))];
    3.10  
    3.11  val pure_appl_syntax =