src/HOL/TLA/Action.thy
changeset 60592 c9bd1d902f04
parent 60591 e0b77517f9a9
child 61853 fb7756087101
     1.1 --- a/src/HOL/TLA/Action.thy	Fri Jun 26 15:55:44 2015 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Fri Jun 26 18:51:19 2015 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Copyright:  1998 University of Munich
     1.5  *)
     1.6  
     1.7 -section {* The action level of TLA as an Isabelle theory *}
     1.8 +section \<open>The action level of TLA as an Isabelle theory\<close>
     1.9  
    1.10  theory Action
    1.11  imports Stfun
    1.12 @@ -102,7 +102,7 @@
    1.13  
    1.14  (* ================ Functions to "unlift" action theorems into HOL rules ================ *)
    1.15  
    1.16 -ML {*
    1.17 +ML \<open>
    1.18  (* The following functions are specialized versions of the corresponding
    1.19     functions defined in Intensional.ML in that they introduce a
    1.20     "world" parameter of the form (s,t) and apply additional rewrites.
    1.21 @@ -120,14 +120,14 @@
    1.22        Const _ $ (Const (@{const_name Valid}, _) $ _) =>
    1.23                (flatten (action_unlift ctxt th) handle THM _ => th)
    1.24      | _ => th;
    1.25 -*}
    1.26 +\<close>
    1.27  
    1.28  attribute_setup action_unlift =
    1.29 -  {* Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of)) *}
    1.30 +  \<open>Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of))\<close>
    1.31  attribute_setup action_rewrite =
    1.32 -  {* Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of)) *}
    1.33 +  \<open>Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of))\<close>
    1.34  attribute_setup action_use =
    1.35 -  {* Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of)) *}
    1.36 +  \<open>Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of))\<close>
    1.37  
    1.38  
    1.39  (* =========================== square / angle brackets =========================== *)
    1.40 @@ -256,7 +256,7 @@
    1.41  
    1.42  (* ======================= action_simp_tac ============================== *)
    1.43  
    1.44 -ML {*
    1.45 +ML \<open>
    1.46  (* A dumb simplification-based tactic with just a little first-order logic:
    1.47     should plug in only "very safe" rules that can be applied blindly.
    1.48     Note that it applies whatever simplifications are currently active.
    1.49 @@ -267,11 +267,11 @@
    1.50                                      @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
    1.51                        ORELSE' (eresolve_tac ctxt ((map (action_use ctxt) elims)
    1.52                                               @ [conjE,disjE,exE]))));
    1.53 -*}
    1.54 +\<close>
    1.55  
    1.56  (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
    1.57  
    1.58 -ML {*
    1.59 +ML \<open>
    1.60  (* "Enabled A" can be proven as follows:
    1.61     - Assume that we know which state variables are "base variables"
    1.62       this should be expressed by a theorem of the form "basevars (x,y,z,...)".
    1.63 @@ -284,11 +284,11 @@
    1.64  
    1.65  fun enabled_tac ctxt base_vars =
    1.66    clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]);
    1.67 -*}
    1.68 +\<close>
    1.69  
    1.70 -method_setup enabled = {*
    1.71 +method_setup enabled = \<open>
    1.72    Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
    1.73 -*}
    1.74 +\<close>
    1.75  
    1.76  (* Example *)
    1.77