src/FOLP/ex/If.thy
changeset 60770 240563fbf41d
parent 58957 c9e744ea8a38
child 61337 4645502c3c64
--- a/src/FOLP/ex/If.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/FOLP/ex/If.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -9,7 +9,7 @@
   assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
   shows "?p : if(P,Q,R)"
 apply (unfold if_def)
-apply (tactic {* fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1 *})
+apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1\<close>)
 done
 
 schematic_lemma ifE:
@@ -19,7 +19,7 @@
   shows "?p : S"
 apply (insert 1)
 apply (unfold if_def)
-apply (tactic {* fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
+apply (tactic \<open>fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1\<close>)
 done
 
 schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
@@ -30,14 +30,14 @@
 apply (rule ifI)
 oops
 
-ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
+ML \<open>val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}]\<close>
 
 schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
-apply (tactic {* fast_tac @{context} if_cs 1 *})
+apply (tactic \<open>fast_tac @{context} if_cs 1\<close>)
 done
 
 schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
-apply (tactic {* fast_tac @{context} if_cs 1 *})
+apply (tactic \<open>fast_tac @{context} if_cs 1\<close>)
 done
 
 end