src/HOL/TLA/Intensional.thy
changeset 42814 5af15f1e2ef6
parent 42018 878f33040280
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/TLA/Intensional.thy	Sun May 15 17:06:35 2011 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Sun May 15 17:45:53 2011 +0200
     1.3 @@ -289,10 +289,10 @@
     1.4      | _ => th
     1.5  *}
     1.6  
     1.7 -attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} ""
     1.8 -attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} ""
     1.9 -attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} ""
    1.10 -attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} ""
    1.11 +attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *}
    1.12 +attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *}
    1.13 +attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
    1.14 +attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *}
    1.15  
    1.16  lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
    1.17    by (simp add: Valid_def)