src/HOL/TLA/Intensional.thy
changeset 30528 7173bf123335
parent 24180 9f818139951b
child 31460 d97fa41cc600
     1.1 --- a/src/HOL/TLA/Intensional.thy	Sun Mar 15 15:59:44 2009 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Sun Mar 15 15:59:44 2009 +0100
     1.3 @@ -294,13 +294,10 @@
     1.4      | _ => th
     1.5  *}
     1.6  
     1.7 -setup {*
     1.8 -  Attrib.add_attributes [
     1.9 -    ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""),
    1.10 -    ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""),
    1.11 -    ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""),
    1.12 -    ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")]
    1.13 -*}
    1.14 +attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} ""
    1.15 +attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} ""
    1.16 +attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} ""
    1.17 +attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} ""
    1.18  
    1.19  lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
    1.20    by (simp add: Valid_def)