# HG changeset patch
# User wenzelm
# Date 1248383617 -7200
# Node ID 910443ff08397e679659ad29bbd2f832913c32fc
# Parent  e2bf2f73b0c87386f33d4c6452394d968be2fc20
removed obsolete ML proof tools;

diff -r e2bf2f73b0c8 -r 910443ff0839 src/HOLCF/FOCUS/Buffer.thy
--- 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 *******************************************************************)