src/FOL/blastdata.ML
author paulson
Tue, 12 Jul 2005 12:49:46 +0200
changeset 16774 515b6020cf5d
parent 11748 06eb315831ff
child 18171 c4f873d65603
permissions -rw-r--r--
experimental code to reduce the amount of type information in blast
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
16774
515b6020cf5d experimental code to reduce the amount of type information in blast
paulson
parents: 11748
diff changeset
     6
  val is_hol    = false
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     7
  val notE	= notE
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     8
  val ccontr	= ccontr
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     9
  val contr_tac = Cla.contr_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    10
  val dup_intr	= Cla.dup_intr
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    11
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    12
  val claset	= Cla.claset
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    13
  val rep_cs    = Cla.rep_cs
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    14
  val cla_modifiers = Cla.cla_modifiers;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    15
  val cla_meth' = Cla.cla_meth'
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    16
  end;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    17
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    18
structure Blast = BlastFun(Blast_Data);
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    19
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    20
val Blast_tac = Blast.Blast_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    21
and blast_tac = Blast.blast_tac;