src/HOL/TLA/Intensional.thy
changeset 60592 c9bd1d902f04
parent 60591 e0b77517f9a9
child 61853 fb7756087101
     1.1 --- a/src/HOL/TLA/Intensional.thy	Fri Jun 26 15:55:44 2015 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Fri Jun 26 18:51:19 2015 +0200
     1.3 @@ -3,8 +3,8 @@
     1.4      Copyright:  1998 University of Munich
     1.5  *)
     1.6  
     1.7 -section {* A framework for "intensional" (possible-world based) logics
     1.8 -  on top of HOL, with lifting of constants and functions *}
     1.9 +section \<open>A framework for "intensional" (possible-world based) logics
    1.10 +  on top of HOL, with lifting of constants and functions\<close>
    1.11  
    1.12  theory Intensional
    1.13  imports Main
    1.14 @@ -147,7 +147,7 @@
    1.15    unl_Rex1:    "w \<Turnstile> \<exists>!x. A x  ==  \<exists>!x. (w \<Turnstile> A x)"
    1.16  
    1.17  
    1.18 -subsection {* Lemmas and tactics for "intensional" logics. *}
    1.19 +subsection \<open>Lemmas and tactics for "intensional" logics.\<close>
    1.20  
    1.21  lemmas intensional_rews [simp] =
    1.22    unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1
    1.23 @@ -203,7 +203,7 @@
    1.24  
    1.25  (* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
    1.26  
    1.27 -ML {*
    1.28 +ML \<open>
    1.29  (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
    1.30     \<turnstile> F = G    becomes   F w = G w
    1.31     \<turnstile> F \<longrightarrow> G  becomes   F w \<longrightarrow> G w
    1.32 @@ -253,15 +253,15 @@
    1.33        Const _ $ (Const (@{const_name Valid}, _) $ _) =>
    1.34                (flatten (int_unlift ctxt th) handle THM _ => th)
    1.35      | _ => th
    1.36 -*}
    1.37 +\<close>
    1.38  
    1.39  attribute_setup int_unlift =
    1.40 -  {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}
    1.41 +  \<open>Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of))\<close>
    1.42  attribute_setup int_rewrite =
    1.43 -  {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}
    1.44 -attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
    1.45 +  \<open>Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of))\<close>
    1.46 +attribute_setup flatten = \<open>Scan.succeed (Thm.rule_attribute (K flatten))\<close>
    1.47  attribute_setup int_use =
    1.48 -  {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
    1.49 +  \<open>Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of))\<close>
    1.50  
    1.51  lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
    1.52    by (simp add: Valid_def)