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)"