--- a/src/HOL/ex/MT.thy Tue Oct 06 17:46:07 2015 +0200
+++ b/src/HOL/ex/MT.thy Tue Oct 06 17:47:28 2015 +0200
@@ -12,7 +12,7 @@
Report 308, Computer Lab, University of Cambridge (1993).
*)
-section {* Milner-Tofte: Co-induction in Relational Semantics *}
+section \<open>Milner-Tofte: Co-induction in Relational Semantics\<close>
theory MT
imports Main
@@ -275,9 +275,9 @@
(* Inference systems *)
(* ############################################################ *)
-ML {*
+ML \<open>
fun infsys_mono_tac ctxt = REPEAT (ares_tac ctxt (@{thms basic_monos} @ [allI, impI]) 1)
-*}
+\<close>
lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))"
by simp
@@ -874,7 +874,7 @@
ve + {ev |-> v} hastyenv te + {ev |=> t}"
apply (unfold hasty_env_def)
apply (simp del: mem_simps add: ve_dom_owr te_dom_owr)
-apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
+apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
apply (case_tac "ev=x")
apply (simp (no_asm_simp) add: ve_app_owr1 te_app_owr1)
apply (simp add: ve_app_owr2 te_app_owr2)
@@ -911,7 +911,7 @@
v_clos(cl) hasty t"
apply (unfold hasty_env_def hasty_def)
apply (drule elab_fix_elim)
-apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
+apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
(*Do a single unfolding of cl*)
apply (frule ssubst) prefer 2 apply assumption
apply (rule hasty_rel_clos_coind)
@@ -919,7 +919,7 @@
apply (simp (no_asm_simp) add: ve_dom_owr te_dom_owr)
apply (simp (no_asm_simp) del: mem_simps add: ve_dom_owr)
-apply (tactic {* safe_tac (put_claset HOL_cs @{context}) *})
+apply (tactic \<open>safe_tac (put_claset HOL_cs @{context})\<close>)
apply (case_tac "ev2=ev1a")
apply (simp (no_asm_simp) del: mem_simps add: ve_app_owr1 te_app_owr1)
apply blast