diff -r c09598a97436 -r d8d85a8172b5 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Filter.thy	Sat Jul 18 22:58:50 2015 +0200
@@ -3,17 +3,17 @@
     Author:     Johannes Hölzl
 *)
 
-section {* Filters on predicates *}
+section \<open>Filters on predicates\<close>
 
 theory Filter
 imports Set_Interval Lifting_Set
 begin
 
-subsection {* Filters *}
+subsection \<open>Filters\<close>
 
-text {*
+text \<open>
   This definition also allows non-proper filters.
-*}
+\<close>
 
 locale is_filter =
   fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
@@ -34,7 +34,7 @@
   using assms by (simp add: Abs_filter_inverse)
 
 
-subsubsection {* Eventually *}
+subsubsection \<open>Eventually\<close>
 
 definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
   where "eventually P F \<longleftrightarrow> Rep_filter F P"
@@ -237,7 +237,7 @@
   frequently_all
   frequently_imp_iff
 
-ML {*
+ML \<open>
   fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
     let
       val mp_thms = facts RL @{thms eventually_rev_mp}
@@ -252,16 +252,16 @@
     in
       CASES cases (resolve_tac ctxt [raw_elim_thm] i)
     end)
-*}
+\<close>
 
-method_setup eventually_elim = {*
+method_setup eventually_elim = \<open>
   Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
-*} "elimination of eventually quantifiers"
+\<close> "elimination of eventually quantifiers"
 
-subsubsection {* Finer-than relation *}
+subsubsection \<open>Finer-than relation\<close>
 
-text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
-filter @{term F'}. *}
+text \<open>@{term "F \<le> F'"} means that filter @{term F} is finer than
+filter @{term F'}.\<close>
 
 instantiation filter :: (type) complete_lattice
 begin
@@ -457,12 +457,12 @@
   then have "\<exists>b\<in>B. \<forall>x\<in>X. b \<le> x"
   proof induct
     case empty then show ?case
-      using `B \<noteq> {}` by auto
+      using \<open>B \<noteq> {}\<close> by auto
   next
     case (insert x X)
     then obtain b where "b \<in> B" "\<And>x. x \<in> X \<Longrightarrow> b \<le> x"
       by auto
-    with `insert x X \<subseteq> B` base[of b x] show ?case
+    with \<open>insert x X \<subseteq> B\<close> base[of b x] show ?case
       by (auto intro: order_trans)
   qed
   then obtain b where "b \<in> B" "b \<le> Inf X"
@@ -477,7 +477,7 @@
   unfolding INF_def by (subst eventually_Inf_base) auto
 
 
-subsubsection {* Map function for filters *}
+subsubsection \<open>Map function for filters\<close>
 
 definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
   where "filtermap f F = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) F)"
@@ -526,7 +526,7 @@
     unfolding le_filter_def eventually_filtermap
     by (subst (1 2) eventually_INF) auto
 qed
-subsubsection {* Standard filters *}
+subsubsection \<open>Standard filters\<close>
 
 definition principal :: "'a set \<Rightarrow> 'a filter" where
   "principal S = Abs_filter (\<lambda>P. \<forall>x\<in>S. P x)"
@@ -576,7 +576,7 @@
 lemma filtermap_principal[simp]: "filtermap f (principal A) = principal (f ` A)"
   unfolding filter_eq_iff eventually_filtermap eventually_principal by simp
 
-subsubsection {* Order filters *}
+subsubsection \<open>Order filters\<close>
 
 definition at_top :: "('a::order) filter"
   where "at_top = (INF k. principal {k ..})"
@@ -648,7 +648,7 @@
   unfolding trivial_limit_def
   by (metis eventually_at_top_linorder order_refl)
 
-subsection {* Sequentially *}
+subsection \<open>Sequentially\<close>
 
 abbreviation sequentially :: "nat filter"
   where "sequentially \<equiv> at_top"
@@ -734,7 +734,7 @@
     by (blast intro: finite_subset)
 qed
 
-subsection {* Limits *}
+subsection \<open>Limits\<close>
 
 definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
   "filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
@@ -828,7 +828,7 @@
   fix i j assume "i \<in> I" "j \<in> I"
   with chain[OF this] show "\<exists>x\<in>I. principal (F x) \<le> inf (principal (F i)) (principal (F j))"
     by auto
-qed (auto simp: eventually_principal `I \<noteq> {}`)
+qed (auto simp: eventually_principal \<open>I \<noteq> {}\<close>)
 
 lemma filterlim_filtermap: "filterlim f F1 (filtermap g F2) = filterlim (\<lambda>x. f (g x)) F1 F2"
   unfolding filterlim_def filtermap_filtermap ..
@@ -850,7 +850,7 @@
     LIM x F. if P x then f x else g x :> G"
   unfolding filterlim_iff eventually_inf_principal by (auto simp: eventually_conj_iff)
 
-subsection {* Limits to @{const at_top} and @{const at_bot} *}
+subsection \<open>Limits to @{const at_top} and @{const at_bot}\<close>
 
 lemma filterlim_at_top:
   fixes f :: "'a \<Rightarrow> ('b::linorder)"
@@ -890,7 +890,7 @@
     have "eventually (\<lambda>x. g z \<le> x) at_top"
       by (rule eventually_ge_at_top)
     with Q show "eventually (\<lambda>x. z \<le> f x) at_top"
-      by eventually_elim (metis mono bij `P z`)
+      by eventually_elim (metis mono bij \<open>P z\<close>)
   qed
 qed
 
@@ -937,7 +937,7 @@
   by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
 
 
-subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
+subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
 
 context begin interpretation lifting_syntax .
 
@@ -1011,7 +1011,7 @@
     fix P' Q'
     assume "G P'" "G Q'"
     moreover
-    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
+    from bi_total_fun[OF \<open>bi_unique A\<close> bi_total_eq, unfolded bi_total_def]
     obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
     have "F P = G P'" "F Q = G Q'" by transfer_prover+
     ultimately have "F (\<lambda>x. P x \<and> Q x)" by(simp add: conj)
@@ -1021,7 +1021,7 @@
     fix P' Q'
     assume "\<forall>x. P' x \<longrightarrow> Q' x" "G P'"
     moreover
-    from bi_total_fun[OF `bi_unique A` bi_total_eq, unfolded bi_total_def]
+    from bi_total_fun[OF \<open>bi_unique A\<close> bi_total_eq, unfolded bi_total_def]
     obtain P Q where [transfer_rule]: "(A ===> op =) P P'" "(A ===> op =) Q Q'" by blast
     have "F P = G P'" by transfer_prover
     moreover have "(\<forall>x. P x \<longrightarrow> Q x) \<longleftrightarrow> (\<forall>x. P' x \<longrightarrow> Q' x)" by transfer_prover
@@ -1046,7 +1046,7 @@
   shows "left_total (rel_filter A)"
 proof(rule left_totalI)
   fix F :: "'a filter"
-  from bi_total_fun[OF bi_unique_fun[OF `bi_total A` bi_unique_eq] bi_total_eq]
+  from bi_total_fun[OF bi_unique_fun[OF \<open>bi_total A\<close> bi_unique_eq] bi_total_eq]
   obtain G where [transfer_rule]: "((A ===> op =) ===> op =) (\<lambda>P. eventually P F) G" 
     unfolding  bi_total_def by blast
   moreover have "is_filter (\<lambda>P. eventually P F) \<longleftrightarrow> is_filter G" by transfer_prover