src/HOL/Library/Complete_Partial_Order2.thy
 changeset 69593 3dda49e08b9d parent 69546 27dae626822b child 70961 70fb697be418
```--- a/src/HOL/Library/Complete_Partial_Order2.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -355,7 +355,7 @@
(* apply cont_intro rules as intro and try to solve
the remaining of the emerging subgoals with simp *)
fun cont_intro_tac ctxt =
-  REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems cont_intro})))
+  REPEAT_ALL_NEW (resolve_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>cont_intro\<close>)))
THEN_ALL_NEW (SOLVED' (simp_tac ctxt))

fun cont_intro_simproc ctxt ct =
@@ -370,9 +370,9 @@
| NONE => NONE
in
case Thm.term_of ct of
-      t as Const (@{const_name ccpo.admissible}, _) \$ _ \$ _ \$ _ => mk_thm t
-    | t as Const (@{const_name mcont}, _) \$ _ \$ _ \$ _ \$ _ \$ _ => mk_thm t
-    | t as Const (@{const_name monotone}, _) \$ _ \$ _ \$ _ => mk_thm t
+      t as Const (\<^const_name>\<open>ccpo.admissible\<close>, _) \$ _ \$ _ \$ _ => mk_thm t
+    | t as Const (\<^const_name>\<open>mcont\<close>, _) \$ _ \$ _ \$ _ \$ _ \$ _ => mk_thm t
+    | t as Const (\<^const_name>\<open>monotone\<close>, _) \$ _ \$ _ \$ _ => mk_thm t
| _ => NONE
end
handle THM _ => NONE
@@ -997,7 +997,7 @@

end

-subsection \<open>@{term "(=)"} as order\<close>
+subsection \<open>\<^term>\<open>(=)\<close> as order\<close>

definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
@@ -1431,13 +1431,13 @@
interpretation lfp: partial_function_definitions "(\<le>) :: _ :: complete_lattice \<Rightarrow> _" Sup
by(rule complete_lattice_partial_function_definitions)

-declaration \<open>Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
+declaration \<open>Partial_Function.init "lfp" \<^term>\<open>lfp.fixp_fun\<close> \<^term>\<open>lfp.mono_body\<close>
@{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>

interpretation gfp: partial_function_definitions "(\<ge>) :: _ :: complete_lattice \<Rightarrow> _" Inf
by(rule complete_lattice_partial_function_definitions_dual)

-declaration \<open>Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
+declaration \<open>Partial_Function.init "gfp" \<^term>\<open>gfp.fixp_fun\<close> \<^term>\<open>gfp.mono_body\<close>
@{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>

lemma insert_mono [partial_function_mono]:```