--- a/src/FOL/simpdata.ML Thu Jul 30 17:59:57 1998 +0200
+++ b/src/FOL/simpdata.ML Thu Jul 30 19:02:52 1998 +0200
@@ -334,11 +334,7 @@
-
-
-
-
-(*** Integration of simplifier with classical reasoner ***)
+(*** integration of simplifier with classical reasoner ***)
(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
fails if there is no equaliy or if an equality is already at the front *)
@@ -353,8 +349,12 @@
if n>0 then rotate_tac n i else no_tac end)
end;
-use "$ISABELLE_HOME/src/Provers/clasimp.ML";
+
+structure Clasimp = ClasimpFun
+ (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
+ val addcongs = op addcongs and delcongs = op delcongs
+ and addSaltern = op addSaltern and addbefore = op addbefore);
+
open Clasimp;
val FOL_css = (FOL_cs, FOL_ss);
-