src/Pure/Proof/proof_rewrite_rules.ML
changeset 17979 09485bdd4b6f
parent 17203 29b2563f5c11
child 18024 853e8219732a
     1.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 21 18:14:58 2005 +0200
     1.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 21 18:14:59 2005 +0200
     1.3 @@ -32,8 +32,8 @@
     1.4      val equal_elim_axm = ax equal_elim_axm [];
     1.5      val symmetric_axm = ax symmetric_axm [propT];
     1.6  
     1.7 -    fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
     1.8 -        (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = SOME prf
     1.9 +    fun rew' _ (PThm (("ProtoPure.goalD", _), _, _, _) % _ %%
    1.10 +        (PThm (("ProtoPure.goalI", _), _, _, _) % _ %% prf)) = SOME prf
    1.11        | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
    1.12          (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
    1.13        | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    1.14 @@ -43,14 +43,14 @@
    1.15        | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    1.16          (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
    1.17            _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
    1.18 -        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    1.19 +        ((tg as PThm (("ProtoPure.goalI", _), _, _, _)) % _ %% prf2)) =
    1.20          SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
    1.21  
    1.22        | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
    1.23          (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
    1.24            (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
    1.25               _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
    1.26 -        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
    1.27 +        ((tg as PThm (("ProtoPure.goalI", _), _, _, _)) % _ %% prf2)) =
    1.28          SOME (tg %> B %% (equal_elim_axm %> A %> B %%
    1.29            (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
    1.30