src/Pure/drule.ML
changeset 4679 24917efb31b5
parent 4610 b1322be47244
child 4691 b159f5d98ceb
--- a/src/Pure/drule.ML	Wed Mar 04 13:15:05 1998 +0100
+++ b/src/Pure/drule.ML	Wed Mar 04 13:16:05 1998 +0100
@@ -51,6 +51,7 @@
   val symmetric_thm	: thm
   val transitive_thm	: thm
   val refl_implies      : thm
+  val symmetric_fun     : thm -> thm
   val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
   val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
 	-> meta_simpset -> thm -> thm
@@ -421,6 +422,8 @@
   in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm))
   end;
 
+fun symmetric_fun thm = thm RS symmetric_thm;
+
 (** Below, a "conversion" has type cterm -> thm **)
 
 val refl_implies = reflexive (cterm_of proto_sign implies);