src/FOL/blastdata.ML
author ballarin
Wed, 19 Jul 2006 19:25:58 +0200
changeset 20168 ed7bced29e1b
parent 18524 57b489b54914
child 21539 c5cf9243ad62
permissions -rw-r--r--
Reimplemented algebra method; now controlled by attribute.
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
18524
57b489b54914 provide equality_name, not_name;
wenzelm
parents: 18171
diff changeset
     6
  val equality_name = "op ="
57b489b54914 provide equality_name, not_name;
wenzelm
parents: 18171
diff changeset
     7
  val not_name = "Not"
7355
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     8
  val notE	= notE
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
     9
  val ccontr	= ccontr
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    10
  val contr_tac = Cla.contr_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    11
  val dup_intr	= Cla.dup_intr
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    12
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    13
  val claset	= Cla.claset
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    14
  val rep_cs    = Cla.rep_cs
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    15
  val cla_modifiers = Cla.cla_modifiers;
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    16
  val cla_meth' = Cla.cla_meth'
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    17
  end;
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
structure Blast = BlastFun(Blast_Data);
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
val Blast_tac = Blast.Blast_tac
4c43090659ca proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
diff changeset
    22
and blast_tac = Blast.blast_tac;