src/Provers/classical.ML
changeset 33369 470a7b233ee5
parent 33339 d41f77196338
child 33519 e31a85f92ce9
     1.1 --- a/src/Provers/classical.ML	Sun Nov 01 15:24:45 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Nov 01 15:44:26 2009 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4                   uwrappers: (string * wrapper) list,
     1.5                   safe0_netpair: netpair, safep_netpair: netpair,
     1.6                   haz_netpair: netpair, dup_netpair: netpair,
     1.7 -                 xtra_netpair: ContextRules.netpair}
     1.8 +                 xtra_netpair: Context_Rules.netpair}
     1.9    val merge_cs          : claset * claset -> claset
    1.10    val addDs             : claset * thm list -> claset
    1.11    val addEs             : claset * thm list -> claset
    1.12 @@ -224,7 +224,7 @@
    1.13           safep_netpair  : netpair,                 (*nets for >0 subgoals*)
    1.14           haz_netpair    : netpair,                 (*nets for unsafe rules*)
    1.15           dup_netpair    : netpair,                 (*nets for duplication*)
    1.16 -         xtra_netpair   : ContextRules.netpair};   (*nets for extra rules*)
    1.17 +         xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
    1.18  
    1.19  (*Desired invariants are
    1.20          safe0_netpair = build safe0_brls,
    1.21 @@ -898,7 +898,7 @@
    1.22  fun haz_dest w = attrib (addE w o make_elim);
    1.23  val haz_elim = attrib o addE;
    1.24  val haz_intro = attrib o addI;
    1.25 -val rule_del = attrib delrule o ContextRules.rule_del;
    1.26 +val rule_del = attrib delrule o Context_Rules.rule_del;
    1.27  
    1.28  
    1.29  end;
    1.30 @@ -914,11 +914,11 @@
    1.31  val setup_attrs =
    1.32    Attrib.setup @{binding swapped} (Scan.succeed swapped)
    1.33      "classical swap of introduction rule" #>
    1.34 -  Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
    1.35 +  Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
    1.36      "declaration of Classical destruction rule" #>
    1.37 -  Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
    1.38 +  Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
    1.39      "declaration of Classical elimination rule" #>
    1.40 -  Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
    1.41 +  Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
    1.42      "declaration of Classical introduction rule" #>
    1.43    Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
    1.44      "remove declaration of intro/elim/dest rule";
    1.45 @@ -931,9 +931,9 @@
    1.46  
    1.47  fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
    1.48    let
    1.49 -    val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
    1.50 +    val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
    1.51      val CS {xtra_netpair, ...} = claset_of ctxt;
    1.52 -    val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
    1.53 +    val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
    1.54      val rules = rules1 @ rules2 @ rules3 @ rules4;
    1.55      val ruleq = Drule.multi_resolves facts rules;
    1.56    in