--- a/src/HOLCF/FOCUS/Buffer.thy Thu Jul 23 23:12:21 2009 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy Thu Jul 23 23:13:37 2009 +0200
@@ -97,16 +97,6 @@
lemma set_cong: "!!X. A = B ==> (x:A) = (x:B)"
by (erule subst, rule refl)
-ML {*
-fun B_prover s tac eqs =
- let val thy = the_context () in
- prove_goal thy s (fn prems => [cut_facts_tac prems 1,
- tac 1, auto_tac (global_claset_of thy, global_simpset_of thy addsimps eqs)])
- end;
-
-fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) [];
-fun prove_backw s thm eqs = B_prover s (rtac (thm RS iffD2)) eqs;
-*}
(**** BufEq *******************************************************************)