src/HOL/HOL.thy
changeset 30609 983e8b6e4e69
parent 30350 d9ecd70b1112
child 30927 bc51b343f80d
     1.1 --- a/src/HOL/HOL.thy	Fri Mar 20 17:04:44 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Mar 20 17:12:37 2009 +0100
     1.3 @@ -1018,12 +1018,10 @@
     1.4    val contr_tac = Classical.contr_tac
     1.5    val dup_intr = Classical.dup_intr
     1.6    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     1.7 -  val claset = Classical.claset
     1.8    val rep_cs = Classical.rep_cs
     1.9    val cla_modifiers = Classical.cla_modifiers
    1.10    val cla_meth' = Classical.cla_meth'
    1.11  );
    1.12 -val Blast_tac = Blast.Blast_tac;
    1.13  val blast_tac = Blast.blast_tac;
    1.14  *}
    1.15