src/Provers/classical.ML
changeset 30528 7173bf123335
parent 30513 1796b8ea88aa
child 30541 9f168bdc468a
     1.1 --- a/src/Provers/classical.ML	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -215,7 +215,7 @@
     1.4  
     1.5  (*Creates rules to eliminate ~A, from rules to introduce A*)
     1.6  fun swapify intrs = intrs RLN (2, [Data.swap]);
     1.7 -fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, Data.swap))) x;
     1.8 +val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
     1.9  
    1.10  (*Uses introduction rules in the normal way, or on negated assumptions,
    1.11    trying rules in order. *)
    1.12 @@ -956,16 +956,17 @@
    1.13  val destN = "dest";
    1.14  val ruleN = "rule";
    1.15  
    1.16 -val setup_attrs = Attrib.add_attributes
    1.17 - [("swapped", swapped, "classical swap of introduction rule"),
    1.18 -  (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
    1.19 -    "declaration of Classical destruction rule"),
    1.20 -  (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
    1.21 -    "declaration of Classical elimination rule"),
    1.22 -  (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
    1.23 -    "declaration of Classical introduction rule"),
    1.24 -  (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
    1.25 -    "remove declaration of intro/elim/dest rule")];
    1.26 +val setup_attrs =
    1.27 +  Attrib.setup @{binding swapped} (Scan.succeed swapped)
    1.28 +    "classical swap of introduction rule" #>
    1.29 +  Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
    1.30 +    "declaration of Classical destruction rule" #>
    1.31 +  Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
    1.32 +    "declaration of Classical elimination rule" #>
    1.33 +  Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
    1.34 +    "declaration of Classical introduction rule" #>
    1.35 +  Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
    1.36 +    "remove declaration of intro/elim/dest rule";
    1.37  
    1.38  
    1.39