src/FOLP/ex/Intuitionistic.thy

 schematic_goal "?p : ~~((P-->Q) | (Q-->P))"
   by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text "Problem ~~17"
 schematic_goal "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
-  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)  -- slow
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)  \<comment> slow
 
 
 subsection \<open>Examples with quantifiers\<close>
 
 text "The converse is classical in the following implications..."

 text "Problem 32"
 schematic_goal "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
         (ALL x. S(x) & R(x) --> L(x)) &  
         (ALL x. M(x) --> R(x))   
     --> (ALL x. P(x) & M(x) --> L(x))"
-  by (tactic "IntPr.best_tac @{context} 1") -- slow
+  by (tactic "IntPr.best_tac @{context} 1") \<comment> slow
 
 text "Problem 39"
 schematic_goal "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
   by (tactic "IntPr.best_tac @{context} 1")
 
 text "Problem 40.  AMENDED"
 schematic_goal "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
               ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
-  by (tactic "IntPr.best_tac @{context} 1") -- slow
+  by (tactic "IntPr.best_tac @{context} 1") \<comment> slow
 
 text "Problem 44"
 schematic_goal "?p : (ALL x. f(x) -->                                    
               (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
               (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    

 
 text "Problem 51"
 schematic_goal
     "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
      (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
-  by (tactic "IntPr.best_tac @{context} 1") -- \<open>60 seconds\<close>
+  by (tactic "IntPr.best_tac @{context} 1") \<comment> \<open>60 seconds\<close>
 
 text "Problem 56"
 schematic_goal "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
   by (tactic "IntPr.best_tac @{context} 1")