--- a/TFL/thms.sml Wed May 21 10:58:24 1997 +0200
+++ b/TFL/thms.sml Wed May 21 10:59:14 1997 +0200
@@ -26,12 +26,10 @@
val COND_CONG = if_cong RS eq_reflection;
- fun C f x y = f y x;
- fun prover thl = [fast_tac HOL_cs 1];
- val P = C (prove_goal HOL.thy) prover;
+ fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
- val eqT = P"(x = True) --> x"
- val rev_eq_mp = P"(x = y) --> y --> x"
- val simp_thm = P"(x-->y) --> (x = x') --> (x' --> y)"
+ val eqT = prove"(x = True) --> x"
+ val rev_eq_mp = prove"(x = y) --> y --> x"
+ val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)"
end;