src/FOL/blastdata.ML
author wenzelm
Sun, 26 Nov 2006 23:43:53 +0100
changeset 21539 c5cf9243ad62
parent 18524 57b489b54914
child 26287 df8e5362cff9
permissions -rw-r--r--
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 18524
diff changeset
     1
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 18524
diff changeset
     2
val ccontr = thm "ccontr";
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     3
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     4
(*** Applying BlastFun to create Blast_tac ***)
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     5
structure Blast_Data = 
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     6
  struct
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     7
  type claset	= Cla.claset
18524
57b489b54914 provide equality_name, not_name;
wenzelm
parents: 18171
diff changeset
     8
  val equality_name = "op ="
57b489b54914 provide equality_name, not_name;
wenzelm
parents: 18171
diff changeset
     9
  val not_name = "Not"
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    10
  val notE	= notE
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    11
  val ccontr	= ccontr
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    12
  val contr_tac = Cla.contr_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    13
  val dup_intr	= Cla.dup_intr
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    14
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    15
  val claset	= Cla.claset
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    16
  val rep_cs    = Cla.rep_cs
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    17
  val cla_modifiers = Cla.cla_modifiers;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    18
  val cla_meth' = Cla.cla_meth'
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    19
  end;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    20
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    21
structure Blast = BlastFun(Blast_Data);
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    22
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    23
val Blast_tac = Blast.Blast_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    24
and blast_tac = Blast.blast_tac;