added type global_theory -- theory or local_theory;
added begin/exit_local_theory;
removed theory_context;
renamed body_context_node to presentation_context;
removed copy (checkpoint twice instead -- avoids unrelated theories);
(*** Applying BlastFun to create Blast_tac ***)
structure Blast_Data =
struct
type claset = Cla.claset
val equality_name = "op ="
val not_name = "Not"
val notE = notE
val ccontr = ccontr
val contr_tac = Cla.contr_tac
val dup_intr = Cla.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
val claset = Cla.claset
val rep_cs = Cla.rep_cs
val cla_modifiers = Cla.cla_modifiers;
val cla_meth' = Cla.cla_meth'
end;
structure Blast = BlastFun(Blast_Data);
val Blast_tac = Blast.Blast_tac
and blast_tac = Blast.blast_tac;