src/HOL/simpdata.ML
changeset 20944 34b2c1bb7178
parent 20932 e65e1234c9d3
child 20973 0b8e436ed071
     1.1 --- a/src/HOL/simpdata.ML	Tue Oct 10 10:34:43 2006 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Oct 10 10:35:24 2006 +0200
     1.3 @@ -6,93 +6,28 @@
     1.4  Instantiation of the generic simplifier for HOL.
     1.5  *)
     1.6  
     1.7 -(* legacy ML bindings *)
     1.8 +(* legacy ML bindings - FIXME get rid of this *)
     1.9  
    1.10  val Eq_FalseI = thm "Eq_FalseI";
    1.11  val Eq_TrueI = thm "Eq_TrueI";
    1.12 -val all_conj_distrib = thm "all_conj_distrib";
    1.13 -val all_simps = thms "all_simps";
    1.14 -val cases_simp = thm "cases_simp";
    1.15 -val conj_assoc = thm "conj_assoc";
    1.16 -val conj_comms = thms "conj_comms";
    1.17 -val conj_commute = thm "conj_commute";
    1.18 -val conj_cong = thm "conj_cong";
    1.19 -val conj_disj_distribL = thm "conj_disj_distribL";
    1.20 -val conj_disj_distribR = thm "conj_disj_distribR";
    1.21 -val conj_left_commute = thm "conj_left_commute";
    1.22  val de_Morgan_conj = thm "de_Morgan_conj";
    1.23  val de_Morgan_disj = thm "de_Morgan_disj";
    1.24 -val disj_assoc = thm "disj_assoc";
    1.25 -val disj_comms = thms "disj_comms";
    1.26 -val disj_commute = thm "disj_commute";
    1.27 -val disj_cong = thm "disj_cong";
    1.28 -val disj_conj_distribL = thm "disj_conj_distribL";
    1.29 -val disj_conj_distribR = thm "disj_conj_distribR";
    1.30 -val disj_left_commute = thm "disj_left_commute";
    1.31 -val disj_not1 = thm "disj_not1";
    1.32 -val disj_not2 = thm "disj_not2";
    1.33 -val eq_ac = thms "eq_ac";
    1.34 -val eq_assoc = thm "eq_assoc";
    1.35 -val eq_commute = thm "eq_commute";
    1.36 -val eq_left_commute = thm "eq_left_commute";
    1.37 -val eq_sym_conv = thm "eq_sym_conv";
    1.38 -val eta_contract_eq = thm "eta_contract_eq";
    1.39 -val ex_disj_distrib = thm "ex_disj_distrib";
    1.40 -val ex_simps = thms "ex_simps";
    1.41 -val if_False = thm "if_False";
    1.42 -val if_P = thm "if_P";
    1.43 -val if_True = thm "if_True";
    1.44 -val if_bool_eq_conj = thm "if_bool_eq_conj";
    1.45 -val if_bool_eq_disj = thm "if_bool_eq_disj";
    1.46 -val if_cancel = thm "if_cancel";
    1.47 -val if_def2 = thm "if_def2";
    1.48 -val if_eq_cancel = thm "if_eq_cancel";
    1.49 -val if_not_P = thm "if_not_P";
    1.50 -val if_splits = thms "if_splits";
    1.51  val iff_conv_conj_imp = thm "iff_conv_conj_imp";
    1.52 -val imp_all = thm "imp_all";
    1.53  val imp_cong = thm "imp_cong";
    1.54 -val imp_conjL = thm "imp_conjL";
    1.55 -val imp_conjR = thm "imp_conjR";
    1.56  val imp_conv_disj = thm "imp_conv_disj";
    1.57  val imp_disj1 = thm "imp_disj1";
    1.58  val imp_disj2 = thm "imp_disj2";
    1.59  val imp_disjL = thm "imp_disjL";
    1.60 -val imp_disj_not1 = thm "imp_disj_not1";
    1.61 -val imp_disj_not2 = thm "imp_disj_not2";
    1.62 -val imp_ex = thm "imp_ex";
    1.63 -val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
    1.64 -val neq_commute = thm "neq_commute";
    1.65 -val not_all = thm "not_all";
    1.66 -val not_ex = thm "not_ex";
    1.67 -val not_iff = thm "not_iff";
    1.68 -val not_imp = thm "not_imp";
    1.69 -val not_not = thm "not_not";
    1.70 -val rev_conj_cong = thm "rev_conj_cong";
    1.71 -val simp_impliesE = thm "simp_impliesI";
    1.72  val simp_impliesI = thm "simp_impliesI";
    1.73  val simp_implies_cong = thm "simp_implies_cong";
    1.74  val simp_implies_def = thm "simp_implies_def";
    1.75 -val simp_thms = thms "simp_thms";
    1.76 -val split_if = thm "split_if";
    1.77 -val split_if_asm = thm "split_if_asm";
    1.78 -val atomize_not = thm"atomize_not";
    1.79  
    1.80  local
    1.81 -val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
    1.82 -              (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
    1.83 -
    1.84 -val iff_allI = allI RS
    1.85 -    prove_goal (the_context()) "!x. P x = Q x ==> (!x. P x) = (!x. Q x)"
    1.86 -               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
    1.87 -val iff_exI = allI RS
    1.88 -    prove_goal (the_context()) "!x. P x = Q x ==> (? x. P x) = (? x. Q x)"
    1.89 -               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
    1.90 -
    1.91 -val all_comm = prove_goal (the_context()) "(!x y. P x y) = (!y x. P x y)"
    1.92 -               (fn _ => [Blast_tac 1])
    1.93 -val ex_comm = prove_goal (the_context()) "(? x y. P x y) = (? y x. P x y)"
    1.94 -               (fn _ => [Blast_tac 1])
    1.95 +  val uncurry = thm "uncurry"
    1.96 +  val iff_allI = thm "iff_allI"
    1.97 +  val iff_exI = thm "iff_exI"
    1.98 +  val all_comm = thm "all_comm"
    1.99 +  val ex_comm = thm "ex_comm"
   1.100  in
   1.101  
   1.102  (*** make simplification procedures for quantifier elimination ***)
   1.103 @@ -109,16 +44,16 @@
   1.104    val conj = HOLogic.conj
   1.105    val imp  = HOLogic.imp
   1.106    (*rules*)
   1.107 -  val iff_reflection = eq_reflection
   1.108 -  val iffI = iffI
   1.109 -  val iff_trans = trans
   1.110 -  val conjI= conjI
   1.111 -  val conjE= conjE
   1.112 -  val impI = impI
   1.113 -  val mp   = mp
   1.114 +  val iff_reflection = HOL.eq_reflection
   1.115 +  val iffI = HOL.iffI
   1.116 +  val iff_trans = HOL.trans
   1.117 +  val conjI= HOL.conjI
   1.118 +  val conjE= HOL.conjE
   1.119 +  val impI = HOL.impI
   1.120 +  val mp   = HOL.mp
   1.121    val uncurry = uncurry
   1.122 -  val exI  = exI
   1.123 -  val exE  = exE
   1.124 +  val exI  = HOL.exI
   1.125 +  val exE  = HOL.exE
   1.126    val iff_allI = iff_allI
   1.127    val iff_exI = iff_exI
   1.128    val all_comm = all_comm
   1.129 @@ -128,63 +63,59 @@
   1.130  end;
   1.131  
   1.132  val defEX_regroup =
   1.133 -  Simplifier.simproc (Theory.sign_of (the_context ()))
   1.134 +  Simplifier.simproc (the_context ())
   1.135      "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
   1.136  
   1.137  val defALL_regroup =
   1.138 -  Simplifier.simproc (Theory.sign_of (the_context ()))
   1.139 +  Simplifier.simproc (the_context ())
   1.140      "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
   1.141  
   1.142  
   1.143 -(*** simproc for proving "(y = x) == False" from prmise "~(x = y)" ***)
   1.144 +(* simproc for proving "(y = x) == False" from premise "~(x = y)" *)
   1.145  
   1.146  val use_neq_simproc = ref true;
   1.147  
   1.148  local
   1.149 -
   1.150 -val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI;
   1.151 -
   1.152 -fun neq_prover sg ss (eq $ lhs $ rhs) =
   1.153 -let
   1.154 -  fun test thm = (case #prop(rep_thm thm) of
   1.155 +  val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI;
   1.156 +  fun neq_prover sg ss (eq $ lhs $ rhs) =
   1.157 +    let
   1.158 +      fun test thm = (case #prop (rep_thm thm) of
   1.159                      _ $ (Not $ (eq' $ l' $ r')) =>
   1.160                        Not = HOLogic.Not andalso eq' = eq andalso
   1.161                        r' aconv lhs andalso l' aconv rhs
   1.162                    | _ => false)
   1.163 -in
   1.164 -  if !use_neq_simproc then
   1.165 -    case Library.find_first test (prems_of_ss ss) of NONE => NONE
   1.166 -    | SOME thm => SOME (thm RS neq_to_EQ_False)
   1.167 -  else NONE
   1.168 -end
   1.169 -
   1.170 +    in if !use_neq_simproc then case find_first test (prems_of_ss ss)
   1.171 +     of NONE => NONE
   1.172 +      | SOME thm => SOME (thm RS neq_to_EQ_False)
   1.173 +     else NONE
   1.174 +    end
   1.175  in
   1.176  
   1.177 -val neq_simproc =
   1.178 -  Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover;
   1.179 +val neq_simproc = Simplifier.simproc (the_context ())
   1.180 +  "neq_simproc" ["x = y"] neq_prover;
   1.181  
   1.182  end;
   1.183  
   1.184  
   1.185 -(*** Simproc for Let ***)
   1.186 +(* Simproc for Let *)
   1.187  
   1.188  val use_let_simproc = ref true;
   1.189  
   1.190  local
   1.191 -val Let_folded = thm "Let_folded";
   1.192 -val Let_unfold = thm "Let_unfold";
   1.193 -
   1.194 -val (f_Let_unfold,x_Let_unfold) =
   1.195 +  val Let_folded = thm "Let_folded";
   1.196 +  val Let_unfold = thm "Let_unfold";
   1.197 +  val (f_Let_unfold,x_Let_unfold) =
   1.198        let val [(_$(f$x)$_)] = prems_of Let_unfold
   1.199 -      in (cterm_of (sign_of (the_context ())) f,cterm_of (sign_of (the_context ())) x) end
   1.200 -val (f_Let_folded,x_Let_folded) =
   1.201 +      in (cterm_of (the_context ()) f,cterm_of (the_context ()) x) end
   1.202 +  val (f_Let_folded,x_Let_folded) =
   1.203        let val [(_$(f$x)$_)] = prems_of Let_folded
   1.204 -      in (cterm_of (sign_of (the_context ())) f, cterm_of (sign_of (the_context ())) x) end;
   1.205 -val g_Let_folded =
   1.206 -      let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end;
   1.207 +      in (cterm_of (the_context ()) f, cterm_of (the_context ()) x) end;
   1.208 +  val g_Let_folded =
   1.209 +      let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (the_context ()) g end;
   1.210  in
   1.211 +
   1.212  val let_simproc =
   1.213 -  Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"]
   1.214 +  Simplifier.simproc (the_context ()) "let_simp" ["Let x f"]
   1.215     (fn sg => fn ss => fn t =>
   1.216       let val ctxt = Simplifier.the_context ss;
   1.217           val ([t'],ctxt') = Variable.import_terms false [t] ctxt;
   1.218 @@ -192,7 +123,7 @@
   1.219        (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
   1.220           if not (!use_let_simproc) then NONE
   1.221           else if is_Free x orelse is_Bound x orelse is_Const x
   1.222 -         then SOME Let_def
   1.223 +         then SOME (thm "Let_def")
   1.224           else
   1.225            let
   1.226               val n = case f of (Abs (x,_,_)) => x | _ => "x";
   1.227 @@ -221,13 +152,14 @@
   1.228             end
   1.229          | _ => NONE)
   1.230       end)
   1.231 +
   1.232  end
   1.233  
   1.234  (*** Case splitting ***)
   1.235  
   1.236  (*Make meta-equalities.  The operator below is Trueprop*)
   1.237  
   1.238 -fun mk_meta_eq r = r RS eq_reflection;
   1.239 +fun mk_meta_eq r = r RS HOL.eq_reflection;
   1.240  fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
   1.241  
   1.242  fun mk_eq th = case concl_of th of
   1.243 @@ -238,7 +170,7 @@
   1.244  (* Expects Trueprop(.) if not == *)
   1.245  
   1.246  fun mk_eq_True r =
   1.247 -  SOME (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
   1.248 +  SOME (r RS HOL.meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => NONE;
   1.249  
   1.250  (* Produce theorems of the form
   1.251    (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)
   1.252 @@ -249,7 +181,7 @@
   1.253      fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
   1.254        | count_imp _ = 0;
   1.255      val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
   1.256 -  in if j = 0 then meta_eq_to_obj_eq
   1.257 +  in if j = 0 then HOL.meta_eq_to_obj_eq
   1.258      else
   1.259        let
   1.260          val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
   1.261 @@ -263,7 +195,7 @@
   1.262          (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
   1.263          (fn prems => EVERY
   1.264           [rewrite_goals_tac [simp_implies_def],
   1.265 -          REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
   1.266 +          REPEAT (ares_tac (HOL.meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])
   1.267        end
   1.268    end;
   1.269  
   1.270 @@ -276,28 +208,19 @@
   1.271       else error "Conclusion of congruence rules must be =-equality"
   1.272     end);
   1.273  
   1.274 -(* Elimination of True from assumptions: *)
   1.275 -
   1.276 -local fun rd s = read_cterm (the_context()) (s, propT);
   1.277 -in val True_implies_equals = standard' (equal_intr
   1.278 -  (implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI))
   1.279 -  (implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P")))));
   1.280 -end;
   1.281 -
   1.282 -
   1.283  structure SplitterData =
   1.284 -  struct
   1.285 +struct
   1.286    structure Simplifier = Simplifier
   1.287    val mk_eq          = mk_eq
   1.288 -  val meta_eq_to_iff = meta_eq_to_obj_eq
   1.289 -  val iffD           = iffD2
   1.290 -  val disjE          = disjE
   1.291 -  val conjE          = conjE
   1.292 -  val exE            = exE
   1.293 -  val contrapos      = contrapos_nn
   1.294 -  val contrapos2     = contrapos_pp
   1.295 -  val notnotD        = notnotD
   1.296 -  end;
   1.297 +  val meta_eq_to_iff = HOL.meta_eq_to_obj_eq
   1.298 +  val iffD           = HOL.iffD2
   1.299 +  val disjE          = HOL.disjE
   1.300 +  val conjE          = HOL.conjE
   1.301 +  val exE            = HOL.exE
   1.302 +  val contrapos      = HOL.contrapos_nn
   1.303 +  val contrapos2     = HOL.contrapos_pp
   1.304 +  val notnotD        = HOL.notnotD
   1.305 +end;
   1.306  
   1.307  structure Splitter = SplitterFun(SplitterData);
   1.308  
   1.309 @@ -310,9 +233,9 @@
   1.310  val Delsplits        = Splitter.Delsplits;
   1.311  
   1.312  val mksimps_pairs =
   1.313 -  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   1.314 -   ("All", [spec]), ("True", []), ("False", []),
   1.315 -   ("HOL.If", [if_bool_eq_conj RS iffD1])];
   1.316 +  [("op -->", [HOL.mp]), ("op &", [thm "conjunct1", thm "conjunct2"]),
   1.317 +   ("All", [HOL.spec]), ("True", []), ("False", []),
   1.318 +   ("HOL.If", [thm "if_bool_eq_conj" RS HOL.iffD1])];
   1.319  
   1.320  (*
   1.321  val mk_atomize:      (string * thm list) list -> thm -> thm list
   1.322 @@ -336,14 +259,14 @@
   1.323  
   1.324  fun unsafe_solver_tac prems =
   1.325    (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   1.326 -  FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];
   1.327 +  FIRST'[resolve_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems), atac, etac HOL.FalseE];
   1.328  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   1.329  
   1.330  (*No premature instantiation of variables during simplification*)
   1.331  fun safe_solver_tac prems =
   1.332    (fn i => REPEAT_DETERM (match_tac [simp_impliesI] i)) THEN'
   1.333 -  FIRST'[match_tac(reflexive_thm::TrueI::refl::prems),
   1.334 -         eq_assume_tac, ematch_tac [FalseE]];
   1.335 +  FIRST'[match_tac(reflexive_thm :: HOL.TrueI :: HOL.refl :: prems),
   1.336 +         eq_assume_tac, ematch_tac [HOL.FalseE]];
   1.337  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   1.338  
   1.339  val HOL_basic_ss =
   1.340 @@ -365,65 +288,42 @@
   1.341    rewriting by "(P|Q --> R) = ((P-->R)&(Q-->R))" might be justified on the
   1.342    grounds that it allows simplification of R in the two cases.*)
   1.343  
   1.344 +local
   1.345 +  val ex_simps = thms "ex_simps";
   1.346 +  val all_simps = thms "all_simps";
   1.347 +  val simp_thms = thms "simp_thms";
   1.348 +  val cases_simp = thm "cases_simp";
   1.349 +  val conj_assoc = thm "conj_assoc";
   1.350 +  val if_False = thm "if_False";
   1.351 +  val if_True = thm "if_True";
   1.352 +  val disj_assoc = thm "disj_assoc";
   1.353 +  val disj_not1 = thm "disj_not1";
   1.354 +  val if_cancel = thm "if_cancel";
   1.355 +  val if_eq_cancel = thm "if_eq_cancel";
   1.356 +  val True_implies_equals = thm "True_implies_equals";
   1.357 +in
   1.358 +
   1.359  val HOL_ss =
   1.360      HOL_basic_ss addsimps
   1.361       ([triv_forall_equality, (* prunes params *)
   1.362         True_implies_equals, (* prune asms `True' *)
   1.363         if_True, if_False, if_cancel, if_eq_cancel,
   1.364         imp_disjL, conj_assoc, disj_assoc,
   1.365 -       de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
   1.366 -       disj_not1, not_all, not_ex, cases_simp,
   1.367 -       thm "the_eq_trivial", the_sym_eq_trivial]
   1.368 +       de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, thm "not_imp",
   1.369 +       disj_not1, thm "not_all", thm "not_ex", cases_simp,
   1.370 +       thm "the_eq_trivial", HOL.the_sym_eq_trivial]
   1.371       @ ex_simps @ all_simps @ simp_thms)
   1.372       addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]
   1.373       addcongs [imp_cong, simp_implies_cong]
   1.374 -     addsplits [split_if];
   1.375 +     addsplits [thm "split_if"];
   1.376 +
   1.377 +end;
   1.378  
   1.379  fun hol_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
   1.380  
   1.381 -
   1.382 -(*Simplifies x assuming c and y assuming ~c*)
   1.383 -val prems = Goalw [if_def]
   1.384 -  "[| b=c; c ==> x=u; ~c ==> y=v |] ==> \
   1.385 -\  (if b then x else y) = (if c then u else v)";
   1.386 -by (asm_simp_tac (HOL_ss addsimps prems) 1);
   1.387 -qed "if_cong";
   1.388 -
   1.389 -(*Prevents simplification of x and y: faster and allows the execution
   1.390 -  of functional programs. NOW THE DEFAULT.*)
   1.391 -Goal "b=c ==> (if b then x else y) = (if c then x else y)";
   1.392 -by (etac arg_cong 1);
   1.393 -qed "if_weak_cong";
   1.394 -
   1.395 -(*Prevents simplification of t: much faster*)
   1.396 -Goal "a = b ==> (let x=a in t(x)) = (let x=b in t(x))";
   1.397 -by (etac arg_cong 1);
   1.398 -qed "let_weak_cong";
   1.399 -
   1.400 -(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
   1.401 -Goal "u = u' ==> (t==u) == (t==u')";
   1.402 -by (asm_simp_tac HOL_ss 1);
   1.403 -qed "eq_cong2";
   1.404 -
   1.405 -Goal "f(if c then x else y) = (if c then f x else f y)";
   1.406 -by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
   1.407 -qed "if_distrib";
   1.408 -
   1.409 -(*For expand_case_tac*)
   1.410 -val prems = Goal "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
   1.411 -by (case_tac "P" 1);
   1.412 -by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
   1.413 -qed "expand_case";
   1.414 -
   1.415 -(*This lemma restricts the effect of the rewrite rule u=v to the left-hand
   1.416 -  side of an equality.  Used in {Integ,Real}/simproc.ML*)
   1.417 -Goal "x=y ==> (x=z) = (y=z)";
   1.418 -by (asm_simp_tac HOL_ss 1);
   1.419 -qed "restrict_to_left";
   1.420 -
   1.421  (* default simpset *)
   1.422  val simpsetup =
   1.423 -  (fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy));
   1.424 +  (fn thy => (change_simpset_of thy (fn _ => HOL_ss); thy));
   1.425  
   1.426  
   1.427  (*** integration of simplifier with classical reasoner ***)
   1.428 @@ -431,7 +331,7 @@
   1.429  structure Clasimp = ClasimpFun
   1.430   (structure Simplifier = Simplifier and Splitter = Splitter
   1.431    and Classical  = Classical and Blast = Blast
   1.432 -  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
   1.433 +  val iffD1 = HOL.iffD1 val iffD2 = HOL.iffD2 val notE = HOL.notE);
   1.434  open Clasimp;
   1.435  
   1.436  val HOL_css = (HOL_cs, HOL_ss);
   1.437 @@ -462,20 +362,20 @@
   1.438      empty_ss setmkeqTrue mk_eq_True
   1.439      setmksimps (mksimps mksimps_pairs)
   1.440      addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
   1.441 -      not_all,not_ex,not_not];
   1.442 +      thm "not_all", thm "not_ex", thm "not_not"];
   1.443    fun prem_nnf_tac i st =
   1.444      full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
   1.445  in
   1.446  fun refute_tac test prep_tac ref_tac =
   1.447    let val refute_prems_tac =
   1.448          REPEAT_DETERM
   1.449 -              (eresolve_tac [conjE, exE] 1 ORELSE
   1.450 +              (eresolve_tac [HOL.conjE, HOL.exE] 1 ORELSE
   1.451                 filter_prems_tac test 1 ORELSE
   1.452 -               etac disjE 1) THEN
   1.453 -        ((etac notE 1 THEN eq_assume_tac 1) ORELSE
   1.454 +               etac HOL.disjE 1) THEN
   1.455 +        ((etac HOL.notE 1 THEN eq_assume_tac 1) ORELSE
   1.456           ref_tac 1);
   1.457    in EVERY'[TRY o filter_prems_tac test,
   1.458 -            REPEAT_DETERM o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,
   1.459 +            REPEAT_DETERM o etac HOL.rev_mp, prep_tac, rtac HOL.ccontr, prem_nnf_tac,
   1.460              SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   1.461    end;
   1.462  end;