# HG changeset patch
# User wenzelm
# Date 1452983755 -3600
# Node ID 0aabc5931361c0e8ea3dd01a262b1e568f739fcc
# Parent  0826f6b6ba092007c088c9be1ec00ccbc4ad182f
tuned syntax;

diff -r 0826f6b6ba09 -r 0aabc5931361 src/HOL/HOLCF/IOA/Pred.thy
--- a/src/HOL/HOLCF/IOA/Pred.thy	Sat Jan 16 23:31:28 2016 +0100
+++ b/src/HOL/HOLCF/IOA/Pred.thy	Sat Jan 16 23:35:55 2016 +0100
@@ -15,8 +15,8 @@
 definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool"  ("_ \<Turnstile> _" [100, 9] 8)
   where "(s \<Turnstile> P) \<longleftrightarrow> P s"
 
-definition valid :: "'a predicate \<Rightarrow> bool"  (*  FIXME ("|-") *)
-  where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
+definition valid :: "'a predicate \<Rightarrow> bool"  ("\<TTurnstile> _" [9] 8)
+  where "(\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
 
 definition NOT :: "'a predicate \<Rightarrow> 'a predicate"  ("\<^bold>\<not> _" [40] 40)
   where "NOT P s \<longleftrightarrow> \<not> P s"
diff -r 0826f6b6ba09 -r 0aabc5931361 src/HOL/HOLCF/IOA/TL.thy
--- a/src/HOL/HOLCF/IOA/TL.thy	Sat Jan 16 23:31:28 2016 +0100
+++ b/src/HOL/HOLCF/IOA/TL.thy	Sat Jan 16 23:35:55 2016 +0100
@@ -12,8 +12,8 @@
 
 type_synonym 'a temporal = "'a Seq predicate"
 
-definition validT :: "'a Seq predicate \<Rightarrow> bool"
-  where "validT P \<longleftrightarrow> (\<forall>s. s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> P))"
+definition validT :: "'a Seq predicate \<Rightarrow> bool"    ("\<^bold>\<TTurnstile> _" [9] 8)
+  where "(\<^bold>\<TTurnstile> P) \<longleftrightarrow> (\<forall>s. s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> P))"
 
 definition unlift :: "'a lift \<Rightarrow> 'a"
   where "unlift x = (case x of Def y \<Rightarrow> y)"
@@ -92,19 +92,19 @@
 
 subsection \<open>TLA Rules by Lamport\<close>
 
-lemma STL1a: "validT P \<Longrightarrow> validT (\<box>P)"
+lemma STL1a: "\<^bold>\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>P)"
   by (simp add: validT_def satisfies_def Box_def tsuffix_def)
 
-lemma STL1b: "valid P \<Longrightarrow> validT (Init P)"
+lemma STL1b: "\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (Init P)"
   by (simp add: valid_def validT_def satisfies_def Init_def)
 
-lemma STL1: "valid P \<Longrightarrow> validT (\<box>(Init P))"
+lemma STL1: "\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>(Init P))"
   apply (rule STL1a)
   apply (erule STL1b)
   done
 
 (*Note that unlift and HD is not at all used!*)
-lemma STL4: "valid (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> validT (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"
+lemma STL4: "\<TTurnstile> (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> \<^bold>\<TTurnstile> (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"
   by (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)
 
 
@@ -144,7 +144,7 @@
 lemma LTL3: "ex \<Turnstile> (Next (F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (Next F) \<^bold>\<longrightarrow> (Next G)"
   by (simp add: Next_def satisfies_def NOT_def IMPLIES_def)
 
-lemma ModusPonens: "validT (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> validT P \<Longrightarrow> validT Q"
+lemma ModusPonens: "\<^bold>\<TTurnstile> (P \<^bold>\<longrightarrow> Q) \<Longrightarrow> \<^bold>\<TTurnstile> P \<Longrightarrow> \<^bold>\<TTurnstile> Q"
   by (simp add: validT_def satisfies_def IMPLIES_def)
 
 end