src/FOL/simpdata.ML
changeset 5219 924359415f09
parent 5115 caf39b7b7a12
child 5220 07f80f447b27
     1.1 --- a/src/FOL/simpdata.ML	Thu Jul 30 17:59:57 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Jul 30 19:02:52 1998 +0200
     1.3 @@ -334,11 +334,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -
     1.8 -
     1.9 -
    1.10 -
    1.11 -(*** Integration of simplifier with classical reasoner ***)
    1.12 +(*** integration of simplifier with classical reasoner ***)
    1.13  
    1.14  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
    1.15     fails if there is no equaliy or if an equality is already at the front *)
    1.16 @@ -353,8 +349,12 @@
    1.17  		if n>0 then rotate_tac n i else no_tac end)
    1.18  end;
    1.19  
    1.20 -use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    1.21 +
    1.22 +structure Clasimp = ClasimpFun
    1.23 + (structure Simplifier = Simplifier and Classical = Cla and Blast = Blast
    1.24 +  val addcongs = op addcongs and delcongs = op delcongs
    1.25 +  and addSaltern = op addSaltern and addbefore = op addbefore);
    1.26 +
    1.27  open Clasimp;
    1.28  
    1.29  val FOL_css = (FOL_cs, FOL_ss);
    1.30 -