--- a/src/FOL/ex/Propositional_Int.thy Thu Dec 31 21:46:31 2015 +0100
+++ b/src/FOL/ex/Propositional_Int.thy Fri Jan 01 10:49:00 2016 +0100
@@ -9,7 +9,7 @@
imports IFOL
begin
-text \<open>commutative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>commutative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
lemma "P \<and> Q \<longrightarrow> Q \<and> P"
by (tactic "IntPr.fast_tac @{context} 1")
@@ -18,7 +18,7 @@
by (tactic "IntPr.fast_tac @{context} 1")
-text \<open>associative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>associative laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
by (tactic "IntPr.fast_tac @{context} 1")
@@ -26,7 +26,7 @@
by (tactic "IntPr.fast_tac @{context} 1")
-text \<open>distributive laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+text \<open>distributive laws of \<open>\<and>\<close> and \<open>\<or>\<close>\<close>
lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
by (tactic "IntPr.fast_tac @{context} 1")
@@ -60,16 +60,16 @@
text \<open>Propositions-as-types\<close>
--- \<open>The combinator K\<close>
+\<comment> \<open>The combinator K\<close>
lemma "P \<longrightarrow> (Q \<longrightarrow> P)"
by (tactic "IntPr.fast_tac @{context} 1")
--- \<open>The combinator S\<close>
+\<comment> \<open>The combinator S\<close>
lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)"
by (tactic "IntPr.fast_tac @{context} 1")
--- \<open>Converse is classical\<close>
+\<comment> \<open>Converse is classical\<close>
lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
by (tactic "IntPr.fast_tac @{context} 1")