--- 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