--- a/src/FOL/IFOL.thy Sun Nov 01 15:24:45 2009 +0100
+++ b/src/FOL/IFOL.thy Sun Nov 01 15:44:26 2009 +0100
@@ -646,7 +646,7 @@
and [Pure.elim 2] = allE notE' impE'
and [Pure.intro] = exI disjI2 disjI1
-setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
+setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
--- a/src/HOL/HOL.thy Sun Nov 01 15:24:45 2009 +0100
+++ b/src/HOL/HOL.thy Sun Nov 01 15:44:26 2009 +0100
@@ -853,7 +853,7 @@
(nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
in
Hypsubst.hypsubst_setup
- #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+ #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
end
*}
--- a/src/HOL/Tools/Function/function.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML Sun Nov 01 15:44:26 2009 +0100
@@ -159,11 +159,11 @@
in
lthy
|> ProofContext.note_thmss ""
- [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+ [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
|> ProofContext.note_thmss ""
- [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+ [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
|> ProofContext.note_thmss ""
- [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
+ [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
[([Goal.norm_result termination], [])])] |> snd
|> Proof.theorem_i NONE afterqed [[(goal, [])]]
end
--- a/src/HOL/Tools/inductive.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Nov 01 15:44:26 2009 +0100
@@ -708,7 +708,7 @@
LocalTheory.notes kind
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~
map (fn th => [([th],
- [Attrib.internal (K (ContextRules.intro_query NONE)),
+ [Attrib.internal (K (Context_Rules.intro_query NONE)),
Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
map (hd o snd);
val (((_, elims'), (_, [induct'])), ctxt2) =
@@ -719,7 +719,7 @@
[Attrib.internal (K (Rule_Cases.case_names cases)),
Attrib.internal (K (Rule_Cases.consumes 1)),
Attrib.internal (K (Induct.cases_pred name)),
- Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
+ Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
LocalTheory.note kind
((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
--- a/src/Provers/blast.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Provers/blast.ML Sun Nov 01 15:44:26 2009 +0100
@@ -55,7 +55,7 @@
swrappers: (string * wrapper) list,
uwrappers: (string * wrapper) list,
safe0_netpair: netpair, safep_netpair: netpair,
- haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
+ haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
val cla_modifiers: Method.modifier parser list
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
end;
--- a/src/Provers/clasimp.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Provers/clasimp.ML Sun Nov 01 15:44:26 2009 +0100
@@ -139,9 +139,9 @@
fun modifier att (x, ths) =
fst (Library.foldl_map (Library.apply [att]) (x, rev ths));
-val addXIs = modifier (ContextRules.intro_query NONE);
-val addXEs = modifier (ContextRules.elim_query NONE);
-val delXs = modifier ContextRules.rule_del;
+val addXIs = modifier (Context_Rules.intro_query NONE);
+val addXEs = modifier (Context_Rules.elim_query NONE);
+val delXs = modifier Context_Rules.rule_del;
in
--- a/src/Provers/classical.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Provers/classical.ML Sun Nov 01 15:44:26 2009 +0100
@@ -45,7 +45,7 @@
uwrappers: (string * wrapper) list,
safe0_netpair: netpair, safep_netpair: netpair,
haz_netpair: netpair, dup_netpair: netpair,
- xtra_netpair: ContextRules.netpair}
+ xtra_netpair: Context_Rules.netpair}
val merge_cs : claset * claset -> claset
val addDs : claset * thm list -> claset
val addEs : claset * thm list -> claset
@@ -224,7 +224,7 @@
safep_netpair : netpair, (*nets for >0 subgoals*)
haz_netpair : netpair, (*nets for unsafe rules*)
dup_netpair : netpair, (*nets for duplication*)
- xtra_netpair : ContextRules.netpair}; (*nets for extra rules*)
+ xtra_netpair : Context_Rules.netpair}; (*nets for extra rules*)
(*Desired invariants are
safe0_netpair = build safe0_brls,
@@ -898,7 +898,7 @@
fun haz_dest w = attrib (addE w o make_elim);
val haz_elim = attrib o addE;
val haz_intro = attrib o addI;
-val rule_del = attrib delrule o ContextRules.rule_del;
+val rule_del = attrib delrule o Context_Rules.rule_del;
end;
@@ -914,11 +914,11 @@
val setup_attrs =
Attrib.setup @{binding swapped} (Scan.succeed swapped)
"classical swap of introduction rule" #>
- Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
+ Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
"declaration of Classical destruction rule" #>
- Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
+ Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
"declaration of Classical elimination rule" #>
- Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
+ Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
"declaration of Classical introduction rule" #>
Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
"remove declaration of intro/elim/dest rule";
@@ -931,9 +931,9 @@
fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
let
- val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
+ val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
val CS {xtra_netpair, ...} = claset_of ctxt;
- val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
+ val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
val rules = rules1 @ rules2 @ rules3 @ rules4;
val ruleq = Drule.multi_resolves facts rules;
in
--- a/src/Pure/Isar/calculation.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Sun Nov 01 15:44:26 2009 +0100
@@ -71,10 +71,11 @@
val sym_add =
Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
- #> ContextRules.elim_query NONE;
+ #> Context_Rules.elim_query NONE;
+
val sym_del =
Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
- #> ContextRules.rule_del;
+ #> Context_Rules.rule_del;
(* symmetric *)
--- a/src/Pure/Isar/context_rules.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML Sun Nov 01 15:44:26 2009 +0100
@@ -33,7 +33,7 @@
attribute context_parser
end;
-structure ContextRules: CONTEXT_RULES =
+structure Context_Rules: CONTEXT_RULES =
struct
--- a/src/Pure/Isar/isar_cmd.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 01 15:44:26 2009 +0100
@@ -371,7 +371,7 @@
in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
val print_rules = Toplevel.unknown_context o
- Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
+ Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of);
val print_trans_rules = Toplevel.unknown_context o
Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
--- a/src/Pure/Isar/method.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/method.ML Sun Nov 01 15:44:26 2009 +0100
@@ -240,7 +240,7 @@
let
val rules =
if not (null arg_rules) then arg_rules
- else flat (ContextRules.find_rules false facts goal ctxt)
+ else flat (Context_Rules.find_rules false facts goal ctxt)
in trace ctxt rules; tac rules facts i end);
fun meth tac x = METHOD (HEADGOAL o tac x);
--- a/src/Pure/Isar/obtain.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/obtain.ML Sun Nov 01 15:44:26 2009 +0100
@@ -157,7 +157,7 @@
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
|> Proof.assume_i
- [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
+ [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
--- a/src/Pure/Isar/specification.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/specification.ML Sun Nov 01 15:44:26 2009 +0100
@@ -313,7 +313,7 @@
ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
ctxt' |> Variable.auto_fixes asm
|> ProofContext.add_assms_i Assumption.assume_export
- [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
+ [((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
|>> (fn [(_, [th])] => th)
end;
--- a/src/Tools/intuitionistic.ML Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Tools/intuitionistic.ML Sun Nov 01 15:44:26 2009 +0100
@@ -25,18 +25,18 @@
fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
-val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
+val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
fun safe_step_tac ctxt =
- ContextRules.Swrap ctxt
+ Context_Rules.Swrap ctxt
(eq_assume_tac ORELSE'
- bires_tac true (ContextRules.netpair_bang ctxt));
+ bires_tac true (Context_Rules.netpair_bang ctxt));
fun unsafe_step_tac ctxt =
- ContextRules.wrap ctxt
+ Context_Rules.wrap ctxt
(assume_tac APPEND'
- bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
- bires_tac false (ContextRules.netpair ctxt));
+ bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
+ bires_tac false (Context_Rules.netpair ctxt));
fun step_tac ctxt i =
REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
@@ -75,13 +75,13 @@
>> (pair (I: Proof.context -> Proof.context) o att);
val modifiers =
- [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
- modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
- modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
- modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
- modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
- modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
- Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
+ [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
+ modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
+ modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
+ modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
+ modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
+ modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
+ Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
in