src/FOL/blastdata.ML
author wenzelm
Sun, 11 Jan 2009 21:49:59 +0100
changeset 29450 ac7f67be7f1f
parent 26287 df8e5362cff9
child 30609 983e8b6e4e69
permissions -rw-r--r--
tuned categories;
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
26287
df8e5362cff9 proper antiquotations;
wenzelm
parents: 21539
diff changeset
     6
  val equality_name = @{const_name "op ="}
df8e5362cff9 proper antiquotations;
wenzelm
parents: 21539
diff changeset
     7
  val not_name = @{const_name Not}
df8e5362cff9 proper antiquotations;
wenzelm
parents: 21539
diff changeset
     8
  val notE	= @{thm notE}
df8e5362cff9 proper antiquotations;
wenzelm
parents: 21539
diff changeset
     9
  val ccontr	= @{thm ccontr}
7355
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;