src/FOL/blastdata.ML
author paulson
Mon, 14 Nov 2005 18:25:34 +0100
changeset 18171 c4f873d65603
parent 16774 515b6020cf5d
child 18524 57b489b54914
permissions -rw-r--r--
removal of is_hol
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     1
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     2
(*** Applying BlastFun to create Blast_tac ***)
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     3
structure Blast_Data = 
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     4
  struct
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     5
  type claset	= Cla.claset
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     6
  val notE	= notE
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     7
  val ccontr	= ccontr
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     8
  val contr_tac = Cla.contr_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     9
  val dup_intr	= Cla.dup_intr
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    10
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    11
  val claset	= Cla.claset
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    12
  val rep_cs    = Cla.rep_cs
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    13
  val cla_modifiers = Cla.cla_modifiers;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    14
  val cla_meth' = Cla.cla_meth'
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    15
  end;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    16
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    17
structure Blast = BlastFun(Blast_Data);
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    18
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    19
val Blast_tac = Blast.Blast_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    20
and blast_tac = Blast.blast_tac;