src/Pure/drule.ML
changeset 47239 0b1829860149
parent 47022 8eac39af4ec0
child 47427 0daa97ed1585
--- a/src/Pure/drule.ML	Sat Mar 31 19:09:59 2012 +0200
+++ b/src/Pure/drule.ML	Sat Mar 31 19:26:23 2012 +0200
@@ -43,7 +43,6 @@
   val reflexive_thm: thm
   val symmetric_thm: thm
   val transitive_thm: thm
-  val symmetric_fun: thm -> thm
   val extensional: thm -> thm
   val asm_rl: thm
   val cut_rl: thm
@@ -400,8 +399,6 @@
     val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
   in store_standard_thm_open (Binding.name "transitive") thm end;
 
-fun symmetric_fun thm = thm RS symmetric_thm;
-
 fun extensional eq =
   let val eq' =
     Thm.abstract_rule "x" (Thm.dest_arg (fst (Thm.dest_equals (cprop_of eq)))) eq