src/FOL/FOL.thy
changeset 32176 893614e2c35c
parent 32171 220abde9962b
child 32261 05e687ddbcee
     1.1 --- a/src/FOL/FOL.thy	Fri Jul 24 21:18:05 2009 +0200
     1.2 +++ b/src/FOL/FOL.thy	Fri Jul 24 21:21:45 2009 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    "~~/src/Provers/clasimp.ML"
     1.5    "~~/src/Tools/induct.ML"
     1.6    ("cladata.ML")
     1.7 -  ("blastdata.ML")
     1.8    ("simpdata.ML")
     1.9  begin
    1.10  
    1.11 @@ -171,7 +170,25 @@
    1.12  setup Cla.setup
    1.13  setup cla_setup
    1.14  
    1.15 -use "blastdata.ML"
    1.16 +ML {*
    1.17 +  structure Blast = Blast
    1.18 +  (
    1.19 +    val thy = @{theory}
    1.20 +    type claset	= Cla.claset
    1.21 +    val equality_name = @{const_name "op ="}
    1.22 +    val not_name = @{const_name Not}
    1.23 +    val notE	= @{thm notE}
    1.24 +    val ccontr	= @{thm ccontr}
    1.25 +    val contr_tac = Cla.contr_tac
    1.26 +    val dup_intr	= Cla.dup_intr
    1.27 +    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    1.28 +    val rep_cs = Cla.rep_cs
    1.29 +    val cla_modifiers = Cla.cla_modifiers
    1.30 +    val cla_meth' = Cla.cla_meth'
    1.31 +  );
    1.32 +  val blast_tac = Blast.blast_tac;
    1.33 +*}
    1.34 +
    1.35  setup Blast.setup
    1.36  
    1.37