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