Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Proofs/Lambda/Commutation.thy
changeset 69597 ff784d5a5bfb
parent 67613 ce654b0e6d69 
--- a/src/HOL/Proofs/Lambda/Commutation.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Proofs/Lambda/Commutation.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -129,9 +129,9 @@
 
 lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
   apply (unfold square_def commute_def diamond_def Church_Rosser_def)
-  apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
+  apply (tactic \<open>safe_tac (put_claset HOL_cs \<^context>)\<close>)
    apply (tactic \<open>
-     blast_tac (put_claset HOL_cs @{context} addIs
+     blast_tac (put_claset HOL_cs \<^context> addIs
        [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
         @{thm rtranclp_converseI}, @{thm conversepI},
         @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1\<close>)
isabelle