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