1.1 --- a/src/FOL/IFOL.thy Sun Nov 01 15:24:45 2009 +0100
1.2 +++ b/src/FOL/IFOL.thy Sun Nov 01 15:44:26 2009 +0100
1.3 @@ -646,7 +646,7 @@
1.4 and [Pure.elim 2] = allE notE' impE'
1.5 and [Pure.intro] = exI disjI2 disjI1
1.6
1.7 -setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
1.8 +setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
1.9
1.10
1.11 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
2.1 --- a/src/HOL/HOL.thy Sun Nov 01 15:24:45 2009 +0100
2.2 +++ b/src/HOL/HOL.thy Sun Nov 01 15:44:26 2009 +0100
2.3 @@ -853,7 +853,7 @@
2.4 (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
2.5 in
2.6 Hypsubst.hypsubst_setup
2.7 - #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
2.8 + #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
2.9 end
2.10 *}
2.11
3.1 --- a/src/HOL/Tools/Function/function.ML Sun Nov 01 15:24:45 2009 +0100
3.2 +++ b/src/HOL/Tools/Function/function.ML Sun Nov 01 15:44:26 2009 +0100
3.3 @@ -159,11 +159,11 @@
3.4 in
3.5 lthy
3.6 |> ProofContext.note_thmss ""
3.7 - [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
3.8 + [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
3.9 |> ProofContext.note_thmss ""
3.10 - [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
3.11 + [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
3.12 |> ProofContext.note_thmss ""
3.13 - [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
3.14 + [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
3.15 [([Goal.norm_result termination], [])])] |> snd
3.16 |> Proof.theorem_i NONE afterqed [[(goal, [])]]
3.17 end
4.1 --- a/src/HOL/Tools/inductive.ML Sun Nov 01 15:24:45 2009 +0100
4.2 +++ b/src/HOL/Tools/inductive.ML Sun Nov 01 15:44:26 2009 +0100
4.3 @@ -708,7 +708,7 @@
4.4 LocalTheory.notes kind
4.5 (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
4.6 map (fn th => [([th],
4.7 - [Attrib.internal (K (ContextRules.intro_query NONE)),
4.8 + [Attrib.internal (K (Context_Rules.intro_query NONE)),
4.9 Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
4.10 map (hd o snd);
4.11 val (((_, elims'), (_, [induct'])), ctxt2) =
4.12 @@ -719,7 +719,7 @@
4.13 [Attrib.internal (K (Rule_Cases.case_names cases)),
4.14 Attrib.internal (K (Rule_Cases.consumes 1)),
4.15 Attrib.internal (K (Induct.cases_pred name)),
4.16 - Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
4.17 + Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
4.18 apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
4.19 LocalTheory.note kind
4.20 ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
5.1 --- a/src/Provers/blast.ML Sun Nov 01 15:24:45 2009 +0100
5.2 +++ b/src/Provers/blast.ML Sun Nov 01 15:44:26 2009 +0100
5.3 @@ -55,7 +55,7 @@
5.4 swrappers: (string * wrapper) list,
5.5 uwrappers: (string * wrapper) list,
5.6 safe0_netpair: netpair, safep_netpair: netpair,
5.7 - haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
5.8 + haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
5.9 val cla_modifiers: Method.modifier parser list
5.10 val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
5.11 end;
6.1 --- a/src/Provers/clasimp.ML Sun Nov 01 15:24:45 2009 +0100
6.2 +++ b/src/Provers/clasimp.ML Sun Nov 01 15:44:26 2009 +0100
6.3 @@ -139,9 +139,9 @@
6.4 fun modifier att (x, ths) =
6.5 fst (Library.foldl_map (Library.apply [att]) (x, rev ths));
6.6
6.7 -val addXIs = modifier (ContextRules.intro_query NONE);
6.8 -val addXEs = modifier (ContextRules.elim_query NONE);
6.9 -val delXs = modifier ContextRules.rule_del;
6.10 +val addXIs = modifier (Context_Rules.intro_query NONE);
6.11 +val addXEs = modifier (Context_Rules.elim_query NONE);
6.12 +val delXs = modifier Context_Rules.rule_del;
6.13
6.14 in
6.15
7.1 --- a/src/Provers/classical.ML Sun Nov 01 15:24:45 2009 +0100
7.2 +++ b/src/Provers/classical.ML Sun Nov 01 15:44:26 2009 +0100
7.3 @@ -45,7 +45,7 @@
7.4 uwrappers: (string * wrapper) list,
7.5 safe0_netpair: netpair, safep_netpair: netpair,
7.6 haz_netpair: netpair, dup_netpair: netpair,
7.7 - xtra_netpair: ContextRules.netpair}
7.8 + xtra_netpair: Context_Rules.netpair}
7.9 val merge_cs : claset * claset -> claset
7.10 val addDs : claset * thm list -> claset
7.11 val addEs : claset * thm list -> claset
7.12 @@ -224,7 +224,7 @@
7.13 safep_netpair : netpair, (*nets for >0 subgoals*)
7.14 haz_netpair : netpair, (*nets for unsafe rules*)
7.15 dup_netpair : netpair, (*nets for duplication*)
7.16 - xtra_netpair : ContextRules.netpair}; (*nets for extra rules*)
7.17 + xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
7.18
7.19 (*Desired invariants are
7.20 safe0_netpair = build safe0_brls,
7.21 @@ -898,7 +898,7 @@
7.22 fun haz_dest w = attrib (addE w o make_elim);
7.23 val haz_elim = attrib o addE;
7.24 val haz_intro = attrib o addI;
7.25 -val rule_del = attrib delrule o ContextRules.rule_del;
7.26 +val rule_del = attrib delrule o Context_Rules.rule_del;
7.27
7.28
7.29 end;
7.30 @@ -914,11 +914,11 @@
7.31 val setup_attrs =
7.32 Attrib.setup @{binding swapped} (Scan.succeed swapped)
7.33 "classical swap of introduction rule" #>
7.34 - Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
7.35 + Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
7.36 "declaration of Classical destruction rule" #>
7.37 - Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
7.38 + Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
7.39 "declaration of Classical elimination rule" #>
7.40 - Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
7.41 + Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
7.42 "declaration of Classical introduction rule" #>
7.43 Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
7.44 "remove declaration of intro/elim/dest rule";
7.45 @@ -931,9 +931,9 @@
7.46
7.47 fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
7.48 let
7.49 - val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
7.50 + val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
7.51 val CS {xtra_netpair, ...} = claset_of ctxt;
7.52 - val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
7.53 + val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
7.54 val rules = rules1 @ rules2 @ rules3 @ rules4;
7.55 val ruleq = Drule.multi_resolves facts rules;
7.56 in
8.1 --- a/src/Pure/Isar/calculation.ML Sun Nov 01 15:24:45 2009 +0100
8.2 +++ b/src/Pure/Isar/calculation.ML Sun Nov 01 15:44:26 2009 +0100
8.3 @@ -71,10 +71,11 @@
8.4
8.5 val sym_add =
8.6 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
8.7 - #> ContextRules.elim_query NONE;
8.8 + #> Context_Rules.elim_query NONE;
8.9 +
8.10 val sym_del =
8.11 Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
8.12 - #> ContextRules.rule_del;
8.13 + #> Context_Rules.rule_del;
8.14
8.15
8.16 (* symmetric *)
9.1 --- a/src/Pure/Isar/context_rules.ML Sun Nov 01 15:24:45 2009 +0100
9.2 +++ b/src/Pure/Isar/context_rules.ML Sun Nov 01 15:44:26 2009 +0100
9.3 @@ -33,7 +33,7 @@
9.4 attribute context_parser
9.5 end;
9.6
9.7 -structure ContextRules: CONTEXT_RULES =
9.8 +structure Context_Rules: CONTEXT_RULES =
9.9 struct
9.10
9.11
10.1 --- a/src/Pure/Isar/isar_cmd.ML Sun Nov 01 15:24:45 2009 +0100
10.2 +++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 01 15:44:26 2009 +0100
10.3 @@ -371,7 +371,7 @@
10.4 in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
10.5
10.6 val print_rules = Toplevel.unknown_context o
10.7 - Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
10.8 + Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of);
10.9
10.10 val print_trans_rules = Toplevel.unknown_context o
10.11 Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
11.1 --- a/src/Pure/Isar/method.ML Sun Nov 01 15:24:45 2009 +0100
11.2 +++ b/src/Pure/Isar/method.ML Sun Nov 01 15:44:26 2009 +0100
11.3 @@ -240,7 +240,7 @@
11.4 let
11.5 val rules =
11.6 if not (null arg_rules) then arg_rules
11.7 - else flat (ContextRules.find_rules false facts goal ctxt)
11.8 + else flat (Context_Rules.find_rules false facts goal ctxt)
11.9 in trace ctxt rules; tac rules facts i end);
11.10
11.11 fun meth tac x = METHOD (HEADGOAL o tac x);
12.1 --- a/src/Pure/Isar/obtain.ML Sun Nov 01 15:24:45 2009 +0100
12.2 +++ b/src/Pure/Isar/obtain.ML Sun Nov 01 15:44:26 2009 +0100
12.3 @@ -157,7 +157,7 @@
12.4 |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
12.5 |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
12.6 |> Proof.assume_i
12.7 - [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
12.8 + [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
12.9 |> `Proof.the_facts
12.10 ||> Proof.chain_facts chain_facts
12.11 ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
13.1 --- a/src/Pure/Isar/specification.ML Sun Nov 01 15:24:45 2009 +0100
13.2 +++ b/src/Pure/Isar/specification.ML Sun Nov 01 15:44:26 2009 +0100
13.3 @@ -313,7 +313,7 @@
13.4 ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
13.5 ctxt' |> Variable.auto_fixes asm
13.6 |> ProofContext.add_assms_i Assumption.assume_export
13.7 - [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
13.8 + [((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
13.9 |>> (fn [(_, [th])] => th)
13.10 end;
13.11
14.1 --- a/src/Tools/intuitionistic.ML Sun Nov 01 15:24:45 2009 +0100
14.2 +++ b/src/Tools/intuitionistic.ML Sun Nov 01 15:44:26 2009 +0100
14.3 @@ -25,18 +25,18 @@
14.4
14.5 fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
14.6
14.7 -val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
14.8 +val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
14.9
14.10 fun safe_step_tac ctxt =
14.11 - ContextRules.Swrap ctxt
14.12 + Context_Rules.Swrap ctxt
14.13 (eq_assume_tac ORELSE'
14.14 - bires_tac true (ContextRules.netpair_bang ctxt));
14.15 + bires_tac true (Context_Rules.netpair_bang ctxt));
14.16
14.17 fun unsafe_step_tac ctxt =
14.18 - ContextRules.wrap ctxt
14.19 + Context_Rules.wrap ctxt
14.20 (assume_tac APPEND'
14.21 - bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
14.22 - bires_tac false (ContextRules.netpair ctxt));
14.23 + bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
14.24 + bires_tac false (Context_Rules.netpair ctxt));
14.25
14.26 fun step_tac ctxt i =
14.27 REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
14.28 @@ -75,13 +75,13 @@
14.29 >> (pair (I: Proof.context -> Proof.context) o att);
14.30
14.31 val modifiers =
14.32 - [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
14.33 - modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
14.34 - modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
14.35 - modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
14.36 - modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
14.37 - modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
14.38 - Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
14.39 + [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
14.40 + modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
14.41 + modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
14.42 + modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
14.43 + modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
14.44 + modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
14.45 + Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
14.46
14.47 in
14.48