--- 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