src/HOL/TLA/Action.thy
changeset 42814 5af15f1e2ef6
parent 42793 88bee9f6eec7
child 47968 3119ad2b5ad3
     1.1 --- a/src/HOL/TLA/Action.thy	Sun May 15 17:06:35 2011 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Sun May 15 17:45:53 2011 +0200
     1.3 @@ -120,9 +120,9 @@
     1.4      | _ => th;
     1.5  *}
     1.6  
     1.7 -attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""
     1.8 -attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""
     1.9 -attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""
    1.10 +attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *}
    1.11 +attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *}
    1.12 +attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *}
    1.13  
    1.14  
    1.15  (* =========================== square / angle brackets =========================== *)
    1.16 @@ -283,7 +283,7 @@
    1.17  
    1.18  method_setup enabled = {*
    1.19    Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
    1.20 -*} ""
    1.21 +*}
    1.22  
    1.23  (* Example *)
    1.24