src/ZF/Resid/Residuals.thy

--- a/src/ZF/Resid/Residuals.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/ZF/Resid/Residuals.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -30,7 +30,7 @@
   "u |> v == THE w. residuals(u,v,w)"
 
 
-subsection{*Setting up rule lists*}
+subsection\<open>Setting up rule lists\<close>
 
 declare Sres.intros [intro]
 declare Sreg.intros [intro]
@@ -61,7 +61,7 @@
 
 declare Sres.intros [simp]
 
-subsection{*residuals is a  partial function*}
+subsection\<open>residuals is a  partial function\<close>
 
 lemma residuals_function [rule_format]:
      "residuals(u,v,w) ==> \<forall>w1. residuals(u,v,w1) \<longrightarrow> w1 = w"
@@ -78,7 +78,7 @@
 apply (blast intro: residuals_function)+
 done
 
-subsection{*Residual function*}
+subsection\<open>Residual function\<close>
 
 lemma res_Var [simp]: "n \<in> nat ==> Var(n) |> Var(n) = Var(n)"
 by (unfold res_func_def, blast)
@@ -108,7 +108,7 @@
      "[|s~t; regular(t)|]==> regular(t) \<longrightarrow> s |> t \<in> redexes"
   by (erule Scomp.induct, auto)
 
-subsection{*Commutation theorem*}
+subsection\<open>Commutation theorem\<close>
 
 lemma sub_comp [simp]: "u<==v ==> u~v"
 by (erule Ssub.induct, simp_all)
@@ -140,7 +140,7 @@
 by (simp add: residuals_subst_rec)
 
 
-subsection{*Residuals are comp and regular*}
+subsection\<open>Residuals are comp and regular\<close>
 
 lemma residuals_preserve_comp [rule_format, simp]:
      "u~v ==> \<forall>w. u~w \<longrightarrow> v~w \<longrightarrow> regular(w) \<longrightarrow> (u|>w) ~ (v|>w)"
@@ -151,7 +151,7 @@
 apply (erule Scomp.induct, auto)
 done
 
-subsection{*Preservation lemma*}
+subsection\<open>Preservation lemma\<close>
 
 lemma union_preserve_comp: "u~v ==> v ~ (u un v)"
 by (erule Scomp.induct, simp_all)
@@ -166,7 +166,7 @@
 
 declare sub_comp [THEN comp_sym, simp]
 
-subsection{*Prism theorem*}
+subsection\<open>Prism theorem\<close>
 
 (* Having more assumptions than needed -- removed below  *)
 lemma prism_l [rule_format]:
@@ -181,7 +181,7 @@
 done
 
 
-subsection{*Levy's Cube Lemma*}
+subsection\<open>Levy's Cube Lemma\<close>
 
 lemma cube: "[|u~v; regular(v); regular(u); w~u|]==>   
            (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"
@@ -196,7 +196,7 @@
 done
 
 
-subsection{*paving theorem*}
+subsection\<open>paving theorem\<close>
 
 lemma paving: "[|w~u; w~v; regular(u); regular(v)|]==>  
            \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &