# HG changeset patch
# User berghofe
# Date 1005297976 -3600
# Node ID 34f72eb7d2db023572770a3d8821105f8a806d11
# Parent  316d11f760f7469c3e67624a38a528626c366fb7
Theorems symmetric, reflexive and transitive are now stored with "open"
derivations.

diff -r 316d11f760f7 -r 34f72eb7d2db src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Nov 09 10:25:10 2001 +0100
+++ b/src/Pure/drule.ML	Fri Nov 09 10:26:16 2001 +0100
@@ -522,17 +522,17 @@
 
 val reflexive_thm =
   let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),logicS)))
-  in store_standard_thm "reflexive" (Thm.reflexive cx) end;
+  in open_store_standard_thm "reflexive" (Thm.reflexive cx) end;
 
 val symmetric_thm =
   let val xy = read_prop "x::'a::logic == y"
-  in store_standard_thm "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
+  in open_store_standard_thm "symmetric" (Thm.implies_intr_hyps (Thm.symmetric (Thm.assume xy))) end;
 
 val transitive_thm =
   let val xy = read_prop "x::'a::logic == y"
       val yz = read_prop "y::'a::logic == z"
       val xythm = Thm.assume xy and yzthm = Thm.assume yz
-  in store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
+  in open_store_standard_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
 
 fun symmetric_fun thm = thm RS symmetric_thm;