src/HOL/blastdata.ML
author haftmann
Tue Oct 10 10:35:24 2006 +0200 (2006-10-10)
changeset 20944 34b2c1bb7178
parent 18524 57b489b54914
child 20973 0b8e436ed071
permissions -rw-r--r--
cleanup basic HOL bootstrap
haftmann@20944
     1
Classical.AddSEs [thm "alt_ex1E"];
wenzelm@7357
     2
wenzelm@7357
     3
structure Blast_Data = 
haftmann@20944
     4
struct
haftmann@20944
     5
  type claset = Classical.claset
wenzelm@18524
     6
  val equality_name = "op ="
wenzelm@18524
     7
  val not_name = "Not"
haftmann@20944
     8
  val notE = HOL.notE
haftmann@20944
     9
  val ccontr = HOL.ccontr
wenzelm@7357
    10
  val contr_tac = Classical.contr_tac
haftmann@20944
    11
  val dup_intr = Classical.dup_intr
wenzelm@7357
    12
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
wenzelm@7357
    13
  val claset	= Classical.claset
haftmann@20944
    14
  val rep_cs = Classical.rep_cs
haftmann@20944
    15
  val cla_modifiers = Classical.cla_modifiers
wenzelm@7357
    16
  val cla_meth' = Classical.cla_meth'
haftmann@20944
    17
end;
wenzelm@7357
    18
wenzelm@7357
    19
structure Blast = BlastFun(Blast_Data);
wenzelm@7357
    20
haftmann@20944
    21
structure HOL =
haftmann@20944
    22
struct
haftmann@20944
    23
haftmann@20944
    24
open HOL;
haftmann@20944
    25
haftmann@20944
    26
val Blast_tac = Blast.Blast_tac;
haftmann@20944
    27
val blast_tac = Blast.blast_tac;
haftmann@20944
    28
haftmann@20944
    29
end;