src/HOL/simpdata.ML
 changeset 7357 d0e16da40ea2 parent 7213 08a354bbc34c child 7369 2d2110cda81e
```     1.1 --- a/src/HOL/simpdata.ML	Wed Aug 25 20:46:40 1999 +0200
1.2 +++ b/src/HOL/simpdata.ML	Wed Aug 25 20:49:02 1999 +0200
1.3 @@ -89,14 +89,14 @@
1.4  end;
1.5
1.6
1.7 -val [prem] = goal HOL.thy "x==y ==> x=y";
1.8 +val [prem] = goal (the_context ()) "x==y ==> x=y";
1.9  by (rewtac prem);
1.10  by (rtac refl 1);
1.11  qed "meta_eq_to_obj_eq";
1.12
1.13  local
1.14
1.15 -  fun prover s = prove_goal HOL.thy s (fn _ => [(Blast_tac 1)]);
1.16 +  fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
1.17
1.18  in
1.19
1.20 @@ -157,7 +157,7 @@
1.21
1.22
1.23  val imp_cong = impI RSN
1.24 -    (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
1.25 +    (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
1.26          (fn _=> [(Blast_tac 1)]) RS mp RS mp);
1.27
1.28  (*Miniscoping: pushing in existential quantifiers*)
1.29 @@ -182,10 +182,10 @@
1.30  (* elimination of existential quantifiers in assumptions *)
1.31
1.32  val ex_all_equiv =
1.33 -  let val lemma1 = prove_goal HOL.thy
1.34 +  let val lemma1 = prove_goal (the_context ())
1.35          "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
1.36          (fn prems => [resolve_tac prems 1, etac exI 1]);
1.37 -      val lemma2 = prove_goalw HOL.thy [Ex_def]
1.38 +      val lemma2 = prove_goalw (the_context ()) [Ex_def]
1.39          "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
1.40          (fn prems => [(REPEAT(resolve_tac prems 1))])
1.41    in equal_intr lemma1 lemma2 end;
1.42 @@ -194,13 +194,13 @@
1.43
1.44  (* Elimination of True from asumptions: *)
1.45
1.46 -val True_implies_equals = prove_goal HOL.thy
1.47 +val True_implies_equals = prove_goal (the_context ())
1.48   "(True ==> PROP P) == PROP P"
1.49  (fn _ => [rtac equal_intr_rule 1, atac 2,
1.50            METAHYPS (fn prems => resolve_tac prems 1) 1,
1.51            rtac TrueI 1]);
1.52
1.53 -fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [(Blast_tac 1)]);
1.54 +fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);
1.55
1.56  prove "conj_commute" "(P&Q) = (Q&P)";
1.57  prove "conj_left_commute" "(P&(Q&R)) = (Q&(P&R))";
1.58 @@ -255,19 +255,19 @@
1.59  (* '&' congruence rule: not included by default!
1.60     May slow rewrite proofs down by as much as 50% *)
1.61
1.62 -let val th = prove_goal HOL.thy
1.63 +let val th = prove_goal (the_context ())
1.64                  "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
1.65                  (fn _=> [(Blast_tac 1)])
1.66  in  bind_thm("conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
1.67
1.68 -let val th = prove_goal HOL.thy
1.69 +let val th = prove_goal (the_context ())
1.70                  "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
1.71                  (fn _=> [(Blast_tac 1)])
1.72  in  bind_thm("rev_conj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
1.73
1.74  (* '|' congruence rule: not included by default! *)
1.75
1.76 -let val th = prove_goal HOL.thy
1.77 +let val th = prove_goal (the_context ())
1.78                  "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
1.79                  (fn _=> [(Blast_tac 1)])
1.80  in  bind_thm("disj_cong",standard (impI RSN (2, th RS mp RS mp)))  end;
1.81 @@ -358,10 +358,10 @@
1.82
1.83  local
1.84  val ex_pattern =
1.85 -  Thm.read_cterm (Theory.sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
1.86 +  Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)",HOLogic.boolT)
1.87
1.88  val all_pattern =
1.89 -  Thm.read_cterm (Theory.sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
1.90 +  Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
1.91
1.92  in
1.93  val defEX_regroup =
1.94 @@ -478,7 +478,7 @@
1.95
1.96
1.97  (*For expand_case_tac*)
1.98 -val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
1.99 +val prems = goal (the_context ()) "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
1.100  by (case_tac "P" 1);
1.101  by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
1.102  val expand_case = result();
1.103 @@ -491,9 +491,8 @@
1.104      Simp_tac i;
1.105
1.106
1.107 -(* install implicit simpset *)
1.108 -
1.109 -simpset_ref() := HOL_ss addcongs [if_weak_cong];
1.110 +(* default simpset *)
1.111 +val simpsetup = [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
1.112
1.113
1.114  (*** integration of simplifier with classical reasoner ***)
```