store_standard_thm "norm_hhf_eq";
authorwenzelm
Fri Nov 10 19:09:40 2000 +0100 (2000-11-10)
changeset 10441d727c39c4a4b
parent 10440 2074e62da354
child 10442 8ef083987af9
store_standard_thm "norm_hhf_eq";
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri Nov 10 19:08:30 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Nov 10 19:09:40 2000 +0100
     1.3 @@ -615,7 +615,7 @@
     1.4          |> Thm.forall_intr cx
     1.5          |> Thm.implies_intr cphi
     1.6          |> Thm.implies_intr rhs)
     1.7 -    |> standard |> curry Thm.name_thm "ProtoPure.norm_hhf_eq"
     1.8 +    |> store_standard_thm "norm_hhf_eq"
     1.9    end;
    1.10  
    1.11  
    1.12 @@ -828,7 +828,6 @@
    1.13  (*make an initial proof state, "PROP A ==> (PROP A)" *)
    1.14  fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal;
    1.15  
    1.16 -
    1.17  end;
    1.18  
    1.19