src/HOL/TLA/Action.thy

       Const _ $ (Const ("Intensional.Valid", _) $ _) =>
               (flatten (action_unlift th) handle THM _ => th)
     | _ => th;
 *}
 
-attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""
-attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""
-attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""
+attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *}
+attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *}
+attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *}
 
 
 (* =========================== square / angle brackets =========================== *)
 
 lemma idle_squareI: "(s,t) |= unchanged v ==> (s,t) |= [A]_v"

   clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]);
 *}
 
 method_setup enabled = {*
   Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
-*} ""
+*}
 
 (* Example *)
 
 lemma
   assumes "basevars (x,y,z)"