src/FOLP/FOLP.thy
changeset 69593 3dda49e08b9d
parent 61337 4645502c3c64
child 69605 a96320074298
     1.1 --- a/src/FOLP/FOLP.thy	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/FOLP/FOLP.thy	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -56,8 +56,8 @@
     1.4      and r2: "!!y. y:Q ==> g(y):R"
     1.5    shows "?p : R"
     1.6    apply (rule excluded_middle [THEN disjE])
     1.7 -   apply (tactic \<open>DEPTH_SOLVE (assume_tac @{context} 1 ORELSE
     1.8 -       resolve_tac @{context} [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1)\<close>)
     1.9 +   apply (tactic \<open>DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE
    1.10 +       resolve_tac \<^context> [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1)\<close>)
    1.11    done
    1.12  
    1.13  (*Double negation law*)
    1.14 @@ -80,10 +80,10 @@
    1.15    apply (insert major)
    1.16    apply (unfold iff_def)
    1.17    apply (rule conjE)
    1.18 -  apply (tactic \<open>DEPTH_SOLVE_1 (eresolve_tac @{context} @{thms impCE} 1 ORELSE
    1.19 -      eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN assume_tac @{context} 1 ORELSE
    1.20 -      assume_tac @{context} 1 ORELSE
    1.21 -      resolve_tac @{context} [@{thm r1}, @{thm r2}] 1)\<close>)+
    1.22 +  apply (tactic \<open>DEPTH_SOLVE_1 (eresolve_tac \<^context> @{thms impCE} 1 ORELSE
    1.23 +      eresolve_tac \<^context> [@{thm notE}, @{thm impE}] 1 THEN assume_tac \<^context> 1 ORELSE
    1.24 +      assume_tac \<^context> 1 ORELSE
    1.25 +      resolve_tac \<^context> [@{thm r1}, @{thm r2}] 1)\<close>)+
    1.26    done
    1.27  
    1.28  
    1.29 @@ -135,7 +135,7 @@
    1.30    "?p2 : ~P | P"
    1.31    "?p3 : ~ ~ P <-> P"
    1.32    "?p4 : (~P --> P) <-> P"
    1.33 -  apply (tactic \<open>ALLGOALS (Cla.fast_tac @{context} FOLP_cs)\<close>)
    1.34 +  apply (tactic \<open>ALLGOALS (Cla.fast_tac \<^context> FOLP_cs)\<close>)
    1.35    done
    1.36  
    1.37  ML_file "simpdata.ML"