norm_hhf_eq is now stored using open_store_standard_thm.
authorberghofe
Wed Oct 31 19:32:05 2001 +0100 (2001-10-31)
changeset 11997402ae1a172ae
parent 11996 b409a8cbe1fb
child 11998 b14e7686ce84
norm_hhf_eq is now stored using open_store_standard_thm.
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Wed Oct 31 01:28:39 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Oct 31 19:32:05 2001 +0100
     1.3 @@ -661,7 +661,7 @@
     1.4          |> Thm.forall_intr cx
     1.5          |> Thm.implies_intr cphi
     1.6          |> Thm.implies_intr rhs)
     1.7 -    |> store_standard_thm "norm_hhf_eq"
     1.8 +    |> open_store_standard_thm "norm_hhf_eq"
     1.9    end;
    1.10  
    1.11