Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Sequents/Modal0.thy
changeset 61386 0a29a984a91b
parent 61385 538100cc4399
child 62144 bdab93ccfaf8 
--- a/src/Sequents/Modal0.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/Modal0.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -43,12 +43,12 @@
 
 lemmas rewrite_rls = strimp_def streqv_def
 
-lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F;  $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
+lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F;  $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
   apply (unfold iff_def)
   apply (assumption | rule conjR impR)+
   done
 
-lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q;  $H,Q,P,$G |- $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q;  $H,Q,P,$G \<turnstile> $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E"
   apply (unfold iff_def)
   apply (assumption | rule conjL impL basic)+
   done
isabelle