src/FOLP/FOLP.thy

   assumes major: "p:P-->Q"
     and r1: "!!x. x:~P ==> f(x):R"
     and r2: "!!y. y:Q ==> g(y):R"
   shows "?p : R"
   apply (rule excluded_middle [THEN disjE])
-   apply (tactic \<open>DEPTH_SOLVE (assume_tac @{context} 1 ORELSE
-       resolve_tac @{context} [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1)\<close>)
+   apply (tactic \<open>DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE
+       resolve_tac \<^context> [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1)\<close>)
   done
 
 (*Double negation law*)
 schematic_goal notnotD: "p:~~P ==> ?p : P"
   apply (rule classical)

     and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
   shows "?p : R"
   apply (insert major)
   apply (unfold iff_def)
   apply (rule conjE)
-  apply (tactic \<open>DEPTH_SOLVE_1 (eresolve_tac @{context} @{thms impCE} 1 ORELSE
-      eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN assume_tac @{context} 1 ORELSE
-      assume_tac @{context} 1 ORELSE
-      resolve_tac @{context} [@{thm r1}, @{thm r2}] 1)\<close>)+
+  apply (tactic \<open>DEPTH_SOLVE_1 (eresolve_tac \<^context> @{thms impCE} 1 ORELSE
+      eresolve_tac \<^context> [@{thm notE}, @{thm impE}] 1 THEN assume_tac \<^context> 1 ORELSE
+      assume_tac \<^context> 1 ORELSE
+      resolve_tac \<^context> [@{thm r1}, @{thm r2}] 1)\<close>)+
   done
 
 
 (*Should be used as swap since ~P becomes redundant*)
 schematic_goal swap:

 schematic_goal cla_rews:
   "?p1 : P | ~P"
   "?p2 : ~P | P"
   "?p3 : ~ ~ P <-> P"
   "?p4 : (~P --> P) <-> P"
-  apply (tactic \<open>ALLGOALS (Cla.fast_tac @{context} FOLP_cs)\<close>)
+  apply (tactic \<open>ALLGOALS (Cla.fast_tac \<^context> FOLP_cs)\<close>)
   done
 
 ML_file "simpdata.ML"
 
 end