# HG changeset patch
# User wenzelm
# Date 1329840593 -3600
# Node ID 1bc7e91a5c7794fb6a268794db0f2cff0162316a
# Parent  1152f98902e771feb8132ba470cdc910e8b7e3cf# Parent  e5438c5797ae799e9030c1d9cf377cf9fdac1c20
merged

diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/Library/Float.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -9,8 +9,7 @@
 imports Complex_Main Lattice_Algebras
 begin
 
-definition
-  pow2 :: "int \<Rightarrow> real" where
+definition pow2 :: "int \<Rightarrow> real" where
   [simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
 
 datatype float = Float int int
@@ -30,17 +29,20 @@
 primrec scale :: "float \<Rightarrow> int" where
   "scale (Float a b) = b"
 
-instantiation float :: zero begin
+instantiation float :: zero
+begin
 definition zero_float where "0 = Float 0 0"
 instance ..
 end
 
-instantiation float :: one begin
+instantiation float :: one
+begin
 definition one_float where "1 = Float 1 0"
 instance ..
 end
 
-instantiation float :: number begin
+instantiation float :: number
+begin
 definition number_of_float where "number_of n = Float n 0"
 instance ..
 end
@@ -124,13 +126,13 @@
   by (auto simp add: pow2_def)
 
 lemma pow2_int: "pow2 (int c) = 2^c"
-by (simp add: pow2_def)
+  by (simp add: pow2_def)
 
-lemma zero_less_pow2[simp]:
-  "0 < pow2 x"
+lemma zero_less_pow2[simp]: "0 < pow2 x"
   by (simp add: pow2_powr)
 
-lemma normfloat_imp_odd_or_zero: "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
+lemma normfloat_imp_odd_or_zero:
+  "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
 proof (induct f rule: normfloat.induct)
   case (1 u v)
   from 1 have ab: "normfloat (Float u v) = Float a b" by auto
@@ -169,7 +171,7 @@
 
 lemma float_eq_odd_helper: 
   assumes odd: "odd a'"
-  and floateq: "real (Float a b) = real (Float a' b')"
+    and floateq: "real (Float a b) = real (Float a' b')"
   shows "b \<le> b'"
 proof - 
   from odd have "a' \<noteq> 0" by auto
@@ -191,8 +193,8 @@
 
 lemma float_eq_odd: 
   assumes odd1: "odd a"
-  and odd2: "odd a'"
-  and floateq: "real (Float a b) = real (Float a' b')"
+    and odd2: "odd a'"
+    and floateq: "real (Float a b) = real (Float a' b')"
   shows "a = a' \<and> b = b'"
 proof -
   from 
@@ -216,7 +218,7 @@
   have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg])
   {
     assume odd: "odd a"
-    then have "a \<noteq> 0" by (simp add: even_def, arith)
+    then have "a \<noteq> 0" by (simp add: even_def) arith
     with float_eq have "a' \<noteq> 0" by auto
     with ab' have "odd a'" by simp
     from odd this float_eq have "a = a' \<and> b = b'" by (rule float_eq_odd)
@@ -236,7 +238,8 @@
     done
 qed
 
-instantiation float :: plus begin
+instantiation float :: plus
+begin
 fun plus_float where
 [simp del]: "(Float a_m a_e) + (Float b_m b_e) = 
      (if a_e \<le> b_e then Float (a_m + b_m * 2^(nat(b_e - a_e))) a_e 
@@ -244,17 +247,20 @@
 instance ..
 end
 
-instantiation float :: uminus begin
+instantiation float :: uminus
+begin
 primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
 instance ..
 end
 
-instantiation float :: minus begin
-definition minus_float where [simp del]: "(z::float) - w = z + (- w)"
+instantiation float :: minus
+begin
+definition minus_float where "(z::float) - w = z + (- w)"
 instance ..
 end
 
-instantiation float :: times begin
+instantiation float :: times
+begin
 fun times_float where [simp del]: "(Float a_m a_e) * (Float b_m b_e) = Float (a_m * b_m) (a_e + b_e)"
 instance ..
 end
@@ -265,7 +271,8 @@
 primrec float_nprt :: "float \<Rightarrow> float" where
   "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" 
 
-instantiation float :: ord begin
+instantiation float :: ord
+begin
 definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w"
 definition less_float_def: "z < (w :: float) \<equiv> real z < real w"
 instance ..
@@ -276,7 +283,7 @@
       auto simp add: pow2_int[symmetric] pow2_add[symmetric])
 
 lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
-  by (cases a) (simp add: uminus_float.simps)
+  by (cases a) simp
 
 lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
   by (cases a, cases b) (simp add: minus_float_def)
@@ -285,7 +292,7 @@
   by (cases a, cases b) (simp add: times_float.simps pow2_add)
 
 lemma real_of_float_0[simp]: "real (0 :: float) = 0"
-  by (auto simp add: zero_float_def float_zero)
+  by (auto simp add: zero_float_def)
 
 lemma real_of_float_1[simp]: "real (1 :: float) = 1"
   by (auto simp add: one_float_def)
@@ -1161,16 +1168,20 @@
 qed
 
 definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
-"lb_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
-    l = bitlen m - int prec
-  in if l > 0 then Float (m div (2^nat l)) (e + l)
-              else Float m e)"
+  "lb_mult prec x y =
+    (case normfloat (x * y) of Float m e \<Rightarrow>
+      let
+        l = bitlen m - int prec
+      in if l > 0 then Float (m div (2^nat l)) (e + l)
+                  else Float m e)"
 
 definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
-"ub_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
-    l = bitlen m - int prec
-  in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
-              else Float m e)"
+  "ub_mult prec x y =
+    (case normfloat (x * y) of Float m e \<Rightarrow>
+      let
+        l = bitlen m - int prec
+      in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
+                  else Float m e)"
 
 lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)"
 proof (cases "normfloat (x * y)")
@@ -1225,7 +1236,8 @@
 primrec float_abs :: "float \<Rightarrow> float" where
   "float_abs (Float m e) = Float \<bar>m\<bar> e"
 
-instantiation float :: abs begin
+instantiation float :: abs
+begin
 definition abs_float_def: "\<bar>x\<bar> = float_abs x"
 instance ..
 end
@@ -1290,10 +1302,10 @@
 declare ceiling_fl.simps[simp del]
 
 definition lb_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
-"lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
+  "lb_mod prec x ub lb = x - ceiling_fl (float_divr prec x lb) * ub"
 
 definition ub_mod :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
-"ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
+  "ub_mod prec x ub lb = x - floor_fl (float_divl prec x ub) * lb"
 
 lemma lb_mod: fixes k :: int assumes "0 \<le> real x" and "real k * y \<le> real x" (is "?k * y \<le> ?x")
   assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
@@ -1307,7 +1319,9 @@
   finally show ?thesis unfolding lb_mod_def real_of_float_sub real_of_float_mult by auto
 qed
 
-lemma ub_mod: fixes k :: int and x :: float assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y")
+lemma ub_mod:
+  fixes k :: int and x :: float
+  assumes "0 \<le> real x" and "real x \<le> real k * y" (is "?x \<le> ?k * y")
   assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
   shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
 proof -
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -2,8 +2,8 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-header{* A formalization of the fraction field of any integral domain 
-         A generalization of Rat.thy from int to any integral domain *}
+header{* A formalization of the fraction field of any integral domain;
+         generalization of theory Rat from int to any integral domain *}
 
 theory Fraction_Field
 imports Main
@@ -14,7 +14,7 @@
 subsubsection {* Construction of the type of fractions *}
 
 definition fractrel :: "(('a::idom * 'a ) * ('a * 'a)) set" where
-  "fractrel == {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
+  "fractrel = {(x, y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
 
 lemma fractrel_iff [simp]:
   "(x, y) \<in> fractrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
@@ -70,8 +70,7 @@
 
 subsubsection {* Representation and basic operations *}
 
-definition
-  Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
+definition Fract :: "'a::idom \<Rightarrow> 'a \<Rightarrow> 'a fract" where
   "Fract a b = Abs_fract (fractrel `` {if b = 0 then (0, 1) else (a, b)})"
 
 code_datatype Fract
@@ -95,14 +94,11 @@
 instantiation fract :: (idom) "{comm_ring_1, power}"
 begin
 
-definition
-  Zero_fract_def [code_unfold]: "0 = Fract 0 1"
+definition Zero_fract_def [code_unfold]: "0 = Fract 0 1"
 
-definition
-  One_fract_def [code_unfold]: "1 = Fract 1 1"
+definition One_fract_def [code_unfold]: "1 = Fract 1 1"
 
-definition
-  add_fract_def:
+definition add_fract_def:
   "q + r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
     fractrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
 
@@ -117,8 +113,7 @@
   with assms show ?thesis by (simp add: Fract_def add_fract_def UN_fractrel2)
 qed
 
-definition
-  minus_fract_def:
+definition minus_fract_def:
   "- q = Abs_fract (\<Union>x \<in> Rep_fract q. fractrel `` {(- fst x, snd x)})"
 
 lemma minus_fract [simp, code]: "- Fract a b = Fract (- a) (b::'a::idom)"
@@ -131,16 +126,14 @@
 lemma minus_fract_cancel [simp]: "Fract (- a) (- b) = Fract a b"
   by (cases "b = 0") (simp_all add: eq_fract)
 
-definition
-  diff_fract_def: "q - r = q + - (r::'a fract)"
+definition diff_fract_def: "q - r = q + - (r::'a fract)"
 
 lemma diff_fract [simp]:
   assumes "b \<noteq> 0" and "d \<noteq> 0"
   shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
   using assms by (simp add: diff_fract_def diff_minus)
 
-definition
-  mult_fract_def:
+definition mult_fract_def:
   "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
     fractrel``{(fst x * fst y, snd x * snd y)})"
 
@@ -238,8 +231,7 @@
 instantiation fract :: (idom) field_inverse_zero
 begin
 
-definition
-  inverse_fract_def:
+definition inverse_fract_def:
   "inverse q = Abs_fract (\<Union>x \<in> Rep_fract q.
      fractrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
 
@@ -252,8 +244,7 @@
   then show ?thesis by (simp add: Fract_def inverse_fract_def UN_fractrel)
 qed
 
-definition
-  divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
+definition divide_fract_def: "q / r = q * inverse (r:: 'a fract)"
 
 lemma divide_fract [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   by (simp add: divide_fract_def)
@@ -261,14 +252,15 @@
 instance proof
   fix q :: "'a fract"
   assume "q \<noteq> 0"
-  then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero)
-    by (simp_all add: mult_fract  inverse_fract fract_expand eq_fract mult_commute)
+  then show "inverse q * q = 1"
+    by (cases q rule: Fract_cases_nonzero)
+      (simp_all add: fract_expand eq_fract mult_commute)
 next
   fix q r :: "'a fract"
   show "q / r = q * inverse r" by (simp add: divide_fract_def)
 next
-  show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
-    (simp add: fract_collapse)
+  show "inverse 0 = (0:: 'a fract)"
+    by (simp add: fract_expand) (simp add: fract_collapse)
 qed
 
 end
@@ -292,7 +284,7 @@
     have "?le a b c d = ?le (a * x) (b * x) c d"
     proof -
       from x have "0 < x * x" by (auto simp add: zero_less_mult_iff)
-      hence "?le a b c d =
+      then have "?le a b c d =
           ((a * d) * (b * d) * (x * x) \<le> (c * b) * (b * d) * (x * x))"
         by (simp add: mult_le_cancel_right)
       also have "... = ?le (a * x) (b * x) c d"
@@ -304,7 +296,7 @@
   let ?D = "b * d" and ?D' = "b' * d'"
   from neq have D: "?D \<noteq> 0" by simp
   from neq have "?D' \<noteq> 0" by simp
-  hence "?le a b c d = ?le (a * ?D') (b * ?D') c d"
+  then have "?le a b c d = ?le (a * ?D') (b * ?D') c d"
     by (rule le_factor)
   also have "... = ((a * b') * ?D * ?D' * d * d' \<le> (c * d') * ?D * ?D' * b * b')"
     by (simp add: mult_ac)
@@ -320,13 +312,11 @@
 instantiation fract :: (linordered_idom) linorder
 begin
 
-definition
-  le_fract_def:
+definition le_fract_def:
    "q \<le> r \<longleftrightarrow> the_elem (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
       {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
 
-definition
-  less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
+definition less_fract_def: "z < (w::'a fract) \<longleftrightarrow> z \<le> w \<and> \<not> w \<le> z"
 
 lemma le_fract [simp]:
   assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -409,28 +399,25 @@
 instantiation fract :: (linordered_idom) "{distrib_lattice, abs_if, sgn_if}"
 begin
 
-definition
-  abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
+definition abs_fract_def: "\<bar>q\<bar> = (if q < 0 then -q else (q::'a fract))"
 
-definition
-  sgn_fract_def:
-    "sgn (q::'a fract) = (if q=0 then 0 else if 0<q then 1 else - 1)"
+definition sgn_fract_def:
+  "sgn (q::'a fract) = (if q=0 then 0 else if 0<q then 1 else - 1)"
 
 theorem abs_fract [simp]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   by (auto simp add: abs_fract_def Zero_fract_def le_less
       eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split)
 
-definition
-  inf_fract_def:
-    "(inf \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
+definition inf_fract_def:
+  "(inf \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
 
-definition
-  sup_fract_def:
-    "(sup \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
+definition sup_fract_def:
+  "(sup \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
 
-instance by intro_classes
-  (auto simp add: abs_fract_def sgn_fract_def
-    min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
+instance
+  by intro_classes
+    (auto simp add: abs_fract_def sgn_fract_def
+      min_max.sup_inf_distrib1 inf_fract_def sup_fract_def)
 
 end
 
@@ -485,8 +472,8 @@
   proof -
     fix a::'a and b::'a
     assume b: "b < 0"
-    hence "0 < -b" by simp
-    hence "P (Fract (-a) (-b))" by (rule step)
+    then have "0 < -b" by simp
+    then have "P (Fract (-a) (-b))" by (rule step)
     thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b])
   qed
   case (Fract a b)
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/Library/Function_Algebras.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -13,9 +13,7 @@
 instantiation "fun" :: (type, plus) plus
 begin
 
-definition
-  "f + g = (\<lambda>x. f x + g x)"
-
+definition "f + g = (\<lambda>x. f x + g x)"
 instance ..
 
 end
@@ -23,9 +21,7 @@
 instantiation "fun" :: (type, zero) zero
 begin
 
-definition
-  "0 = (\<lambda>x. 0)"
-
+definition "0 = (\<lambda>x. 0)"
 instance ..
 
 end
@@ -33,9 +29,7 @@
 instantiation "fun" :: (type, times) times
 begin
 
-definition
-  "f * g = (\<lambda>x. f x * g x)"
-
+definition "f * g = (\<lambda>x. f x * g x)"
 instance ..
 
 end
@@ -43,9 +37,7 @@
 instantiation "fun" :: (type, one) one
 begin
 
-definition
-  "1 = (\<lambda>x. 1)"
-
+definition "1 = (\<lambda>x. 1)"
 instance ..
 
 end
@@ -53,69 +45,70 @@
 
 text {* Additive structures *}
 
-instance "fun" :: (type, semigroup_add) semigroup_add proof
-qed (simp add: plus_fun_def add.assoc)
+instance "fun" :: (type, semigroup_add) semigroup_add
+  by default (simp add: plus_fun_def add.assoc)
 
-instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
-qed (simp_all add: plus_fun_def fun_eq_iff)
+instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
+  by default (simp_all add: plus_fun_def fun_eq_iff)
 
-instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
-qed (simp add: plus_fun_def add.commute)
+instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
+  by default (simp add: plus_fun_def add.commute)
 
-instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
-qed simp
+instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
+  by default simp
 
-instance "fun" :: (type, monoid_add) monoid_add proof
-qed (simp_all add: plus_fun_def zero_fun_def)
+instance "fun" :: (type, monoid_add) monoid_add
+  by default (simp_all add: plus_fun_def zero_fun_def)
 
-instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
-qed simp
+instance "fun" :: (type, comm_monoid_add) comm_monoid_add
+  by default simp
 
 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
 
-instance "fun" :: (type, group_add) group_add proof
-qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+instance "fun" :: (type, group_add) group_add
+  by default
+    (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
 
-instance "fun" :: (type, ab_group_add) ab_group_add proof
-qed (simp_all add: diff_minus)
+instance "fun" :: (type, ab_group_add) ab_group_add
+  by default (simp_all add: diff_minus)
 
 
 text {* Multiplicative structures *}
 
-instance "fun" :: (type, semigroup_mult) semigroup_mult proof
-qed (simp add: times_fun_def mult.assoc)
+instance "fun" :: (type, semigroup_mult) semigroup_mult
+  by default (simp add: times_fun_def mult.assoc)
 
-instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
-qed (simp add: times_fun_def mult.commute)
+instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
+  by default (simp add: times_fun_def mult.commute)
 
-instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
-qed (simp add: times_fun_def)
+instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult
+  by default (simp add: times_fun_def)
 
-instance "fun" :: (type, monoid_mult) monoid_mult proof
-qed (simp_all add: times_fun_def one_fun_def)
+instance "fun" :: (type, monoid_mult) monoid_mult
+  by default (simp_all add: times_fun_def one_fun_def)
 
-instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
-qed simp
+instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
+  by default simp
 
 
 text {* Misc *}
 
 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
 
-instance "fun" :: (type, mult_zero) mult_zero proof
-qed (simp_all add: zero_fun_def times_fun_def)
+instance "fun" :: (type, mult_zero) mult_zero
+  by default (simp_all add: zero_fun_def times_fun_def)
 
-instance "fun" :: (type, zero_neq_one) zero_neq_one proof
-qed (simp add: zero_fun_def one_fun_def fun_eq_iff)
+instance "fun" :: (type, zero_neq_one) zero_neq_one
+  by default (simp add: zero_fun_def one_fun_def fun_eq_iff)
 
 
 text {* Ring structures *}
 
-instance "fun" :: (type, semiring) semiring proof
-qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
+instance "fun" :: (type, semiring) semiring
+  by default (simp_all add: plus_fun_def times_fun_def algebra_simps)
 
-instance "fun" :: (type, comm_semiring) comm_semiring proof
-qed (simp add: plus_fun_def times_fun_def algebra_simps)
+instance "fun" :: (type, comm_semiring) comm_semiring
+  by default (simp add: plus_fun_def times_fun_def algebra_simps)
 
 instance "fun" :: (type, semiring_0) semiring_0 ..
 
@@ -127,8 +120,7 @@
 
 instance "fun" :: (type, semiring_1) semiring_1 ..
 
-lemma of_nat_fun:
-  shows "of_nat n = (\<lambda>x::'a. of_nat n)"
+lemma of_nat_fun: "of_nat n = (\<lambda>x::'a. of_nat n)"
 proof -
   have comp: "comp = (\<lambda>f g x. f (g x))"
     by (rule ext)+ simp
@@ -147,7 +139,8 @@
 
 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
 
-instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
+instance "fun" :: (type, semiring_char_0) semiring_char_0
+proof
   from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
     by (rule inj_fun)
   then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
@@ -168,23 +161,24 @@
 
 text {* Ordereded structures *}
 
-instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
-qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
+instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
+  by default (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
 
 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
 
-instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
-qed (simp add: plus_fun_def le_fun_def)
+instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
+  by default (simp add: plus_fun_def le_fun_def)
 
 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
 
 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
 
-instance "fun" :: (type, ordered_semiring) ordered_semiring proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
+instance "fun" :: (type, ordered_semiring) ordered_semiring
+  by default
+    (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
 
-instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
-qed (fact mult_left_mono)
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
+  by default (fact mult_left_mono)
 
 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
 
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/Library/Ramsey.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -47,11 +47,11 @@
     qed
   } moreover
   { assume "m\<noteq>0" "n\<noteq>0"
-    hence "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
-    from Suc(1)[OF this(1)] Suc(1)[OF this(2)] 
+    then have "k = (m - 1) + n" "k = m + (n - 1)" using `Suc k = m+n` by auto
+    from Suc(1)[OF this(1)] Suc(1)[OF this(2)]
     obtain r1 r2 where "r1\<ge>1" "r2\<ge>1" "?R (m - 1) n r1" "?R m (n - 1) r2"
       by auto
-    hence "r1+r2 \<ge> 1" by arith
+    then have "r1+r2 \<ge> 1" by arith
     moreover
     have "?R m n (r1+r2)" (is "ALL V E. _ \<longrightarrow> ?EX V E m n")
     proof clarify
@@ -62,12 +62,12 @@
       let ?M = "{w : V. w\<noteq>v & {v,w} : E}"
       let ?N = "{w : V. w\<noteq>v & {v,w} ~: E}"
       have "V = insert v (?M \<union> ?N)" using `v : V` by auto
-      hence "card V = card(insert v (?M \<union> ?N))" by metis
+      then have "card V = card(insert v (?M \<union> ?N))" by metis
       also have "\<dots> = card ?M + card ?N + 1" using `finite V`
         by(fastforce intro: card_Un_disjoint)
       finally have "card V = card ?M + card ?N + 1" .
-      hence "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
-      hence "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
+      then have "r1+r2 \<le> card ?M + card ?N + 1" using `r1+r2 \<le> card V` by simp
+      then have "r1 \<le> card ?M \<or> r2 \<le> card ?N" by arith
       moreover
       { assume "r1 \<le> card ?M"
         moreover have "finite ?M" using `finite V` by auto
@@ -82,7 +82,7 @@
           with `R <= V` have "?EX V E m n" by blast
         } moreover
         { assume "?C"
-          hence "clique (insert v R) E" using `R <= ?M`
+          then have "clique (insert v R) E" using `R <= ?M`
            by(auto simp:clique_def insert_commute)
           moreover have "card(insert v R) = m"
             using `?C` `finite R` `v ~: R` `m\<noteq>0` by simp
@@ -102,7 +102,7 @@
           with `R <= V` have "?EX V E m n" by blast
         } moreover
         { assume "?I"
-          hence "indep (insert v R) E" using `R <= ?N`
+          then have "indep (insert v R) E" using `R <= ?N`
             by(auto simp:indep_def insert_commute)
           moreover have "card(insert v R) = n"
             using `?I` `finite R` `v ~: R` `n\<noteq>0` by simp
@@ -124,17 +124,17 @@
     choice_0:   "choice P r 0 = (SOME x. P x)"
   | choice_Suc: "choice P r (Suc n) = (SOME y. P y & (choice P r n, y) \<in> r)"
 
-lemma choice_n: 
+lemma choice_n:
   assumes P0: "P x0"
       and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
   shows "P (choice P r n)"
 proof (induct n)
-  case 0 show ?case by (force intro: someI P0) 
+  case 0 show ?case by (force intro: someI P0)
 next
-  case Suc thus ?case by (auto intro: someI2_ex [OF Pstep]) 
+  case Suc then show ?case by (auto intro: someI2_ex [OF Pstep])
 qed
 
-lemma dependent_choice: 
+lemma dependent_choice:
   assumes trans: "trans r"
       and P0: "P x0"
       and Pstep: "!!x. P x ==> \<exists>y. P y & (x,y) \<in> r"
@@ -144,7 +144,7 @@
   fix n
   show "P (choice P r n)" by (blast intro: choice_n [OF P0 Pstep])
 next
-  have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r" 
+  have PSuc: "\<forall>n. (choice P r n, choice P r (Suc n)) \<in> r"
     using Pstep [OF choice_n [OF P0 Pstep]]
     by (auto intro: someI2_ex)
   fix n m :: nat
@@ -156,8 +156,7 @@
 
 subsubsection {* Partitions of a Set *}
 
-definition
-  part :: "nat => nat => 'a set => ('a set => nat) => bool"
+definition part :: "nat => nat => 'a set => ('a set => nat) => bool"
   --{*the function @{term f} partitions the @{term r}-subsets of the typically
        infinite set @{term Y} into @{term s} distinct categories.*}
 where
@@ -165,52 +164,52 @@
 
 text{*For induction, we decrease the value of @{term r} in partitions.*}
 lemma part_Suc_imp_part:
-     "[| infinite Y; part (Suc r) s Y f; y \<in> Y |] 
+     "[| infinite Y; part (Suc r) s Y f; y \<in> Y |]
       ==> part r s (Y - {y}) (%u. f (insert y u))"
   apply(simp add: part_def, clarify)
   apply(drule_tac x="insert y X" in spec)
   apply(force)
   done
 
-lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f" 
+lemma part_subset: "part r s YY f ==> Y \<subseteq> YY ==> part r s Y f"
   unfolding part_def by blast
-  
+
 
 subsection {* Ramsey's Theorem: Infinitary Version *}
 
-lemma Ramsey_induction: 
+lemma Ramsey_induction:
   fixes s and r::nat
   shows
-  "!!(YY::'a set) (f::'a set => nat). 
+  "!!(YY::'a set) (f::'a set => nat).
       [|infinite YY; part r s YY f|]
-      ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s & 
+      ==> \<exists>Y' t'. Y' \<subseteq> YY & infinite Y' & t' < s &
                   (\<forall>X. X \<subseteq> Y' & finite X & card X = r --> f X = t')"
 proof (induct r)
   case 0
-  thus ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
+  then show ?case by (auto simp add: part_def card_eq_0_iff cong: conj_cong)
 next
-  case (Suc r) 
+  case (Suc r)
   show ?case
   proof -
     from Suc.prems infinite_imp_nonempty obtain yy where yy: "yy \<in> YY" by blast
     let ?ramr = "{((y,Y,t),(y',Y',t')). y' \<in> Y & Y' \<subseteq> Y}"
-    let ?propr = "%(y,Y,t).     
+    let ?propr = "%(y,Y,t).
                  y \<in> YY & y \<notin> Y & Y \<subseteq> YY & infinite Y & t < s
                  & (\<forall>X. X\<subseteq>Y & finite X & card X = r --> (f o insert y) X = t)"
     have infYY': "infinite (YY-{yy})" using Suc.prems by auto
     have partf': "part r s (YY - {yy}) (f \<circ> insert yy)"
       by (simp add: o_def part_Suc_imp_part yy Suc.prems)
-    have transr: "trans ?ramr" by (force simp add: trans_def) 
+    have transr: "trans ?ramr" by (force simp add: trans_def)
     from Suc.hyps [OF infYY' partf']
     obtain Y0 and t0
     where "Y0 \<subseteq> YY - {yy}"  "infinite Y0"  "t0 < s"
           "\<forall>X. X\<subseteq>Y0 \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yy) X = t0"
-        by blast 
+        by blast
     with yy have propr0: "?propr(yy,Y0,t0)" by blast
-    have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr" 
+    have proprstep: "\<And>x. ?propr x \<Longrightarrow> \<exists>y. ?propr y \<and> (x, y) \<in> ?ramr"
     proof -
       fix x
-      assume px: "?propr x" thus "?thesis x"
+      assume px: "?propr x" then show "?thesis x"
       proof (cases x)
         case (fields yx Yx tx)
         then obtain yx' where yx': "yx' \<in> Yx" using px
@@ -223,7 +222,7 @@
         obtain Y' and t'
         where Y': "Y' \<subseteq> Yx - {yx'}"  "infinite Y'"  "t' < s"
                "\<forall>X. X\<subseteq>Y' \<and> finite X \<and> card X = r \<longrightarrow> (f \<circ> insert yx') X = t'"
-            by blast 
+            by blast
         show ?thesis
         proof
           show "?propr (yx',Y',t') & (x, (yx',Y',t')) \<in> ?ramr"
@@ -258,51 +257,51 @@
     show ?thesis
     proof (intro exI conjI)
       show "?gy ` {n. ?gt n = s'} \<subseteq> YY" using pg
-        by (auto simp add: Let_def split_beta) 
+        by (auto simp add: Let_def split_beta)
       show "infinite (?gy ` {n. ?gt n = s'})" using infeqs'
-        by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD) 
+        by (blast intro: inj_gy [THEN subset_inj_on] dest: finite_imageD)
       show "s' < s" by (rule less')
-      show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r 
+      show "\<forall>X. X \<subseteq> ?gy ` {n. ?gt n = s'} & finite X & card X = Suc r
           --> f X = s'"
       proof -
-        {fix X 
+        {fix X
          assume "X \<subseteq> ?gy ` {n. ?gt n = s'}"
             and cardX: "finite X" "card X = Suc r"
-         then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA" 
-             by (auto simp add: subset_image_iff) 
+         then obtain AA where AA: "AA \<subseteq> {n. ?gt n = s'}" and Xeq: "X = ?gy`AA"
+             by (auto simp add: subset_image_iff)
          with cardX have "AA\<noteq>{}" by auto
-         hence AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex) 
+         then have AAleast: "(LEAST x. x \<in> AA) \<in> AA" by (auto intro: LeastI_ex)
          have "f X = s'"
-         proof (cases "g (LEAST x. x \<in> AA)") 
+         proof (cases "g (LEAST x. x \<in> AA)")
            case (fields ya Ya ta)
-           with AAleast Xeq 
-           have ya: "ya \<in> X" by (force intro!: rev_image_eqI) 
-           hence "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
-           also have "... = ta" 
+           with AAleast Xeq
+           have ya: "ya \<in> X" by (force intro!: rev_image_eqI)
+           then have "f X = f (insert ya (X - {ya}))" by (simp add: insert_absorb)
+           also have "... = ta"
            proof -
              have "X - {ya} \<subseteq> Ya"
-             proof 
+             proof
                fix x assume x: "x \<in> X - {ya}"
-               then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA" 
-                 by (auto simp add: Xeq) 
-               hence "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
-               hence lessa': "(LEAST x. x \<in> AA) < a'"
+               then obtain a' where xeq: "x = ?gy a'" and a': "a' \<in> AA"
+                 by (auto simp add: Xeq)
+               then have "a' \<noteq> (LEAST x. x \<in> AA)" using x fields by auto
+               then have lessa': "(LEAST x. x \<in> AA) < a'"
                  using Least_le [of "%x. x \<in> AA", OF a'] by arith
                show "x \<in> Ya" using xeq fields rg [OF lessa'] by auto
              qed
              moreover
              have "card (X - {ya}) = r"
                by (simp add: cardX ya)
-             ultimately show ?thesis 
+             ultimately show ?thesis
                using pg [of "LEAST x. x \<in> AA"] fields cardX
                by (clarsimp simp del:insert_Diff_single)
            qed
            also have "... = s'" using AA AAleast fields by auto
            finally show ?thesis .
          qed}
-        thus ?thesis by blast
-      qed 
-    qed 
+        then show ?thesis by blast
+      qed
+    qed
   qed
 qed
 
@@ -312,7 +311,7 @@
   shows
    "[|infinite Z;
       \<forall>X. X \<subseteq> Z & finite X & card X = r --> f X < s|]
-  ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s 
+  ==> \<exists>Y t. Y \<subseteq> Z & infinite Y & t < s
             & (\<forall>X. X \<subseteq> Y & finite X & card X = r --> f X = t)"
 by (blast intro: Ramsey_induction [unfolded part_def])
 
@@ -326,7 +325,7 @@
 proof -
   have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
     using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
-  obtain Y t 
+  obtain Y t
     where "Y \<subseteq> Z" "infinite Y" "t < s"
           "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
     by (insert Ramsey [OF infZ part2]) auto
@@ -342,39 +341,36 @@
   \cite{Podelski-Rybalchenko}.
 *}
 
-definition
-  disj_wf         :: "('a * 'a)set => bool"
-where
-  "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
+definition disj_wf :: "('a * 'a)set => bool"
+  where "disj_wf r = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r = (\<Union>i<n. T i))"
 
-definition
-  transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
-where
-  "transition_idx s T A =
-    (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
+definition transition_idx :: "[nat => 'a, nat => ('a*'a)set, nat set] => nat"
+  where
+    "transition_idx s T A =
+      (LEAST k. \<exists>i j. A = {i,j} & i<j & (s j, s i) \<in> T k)"
 
 
 lemma transition_idx_less:
     "[|i<j; (s j, s i) \<in> T k; k<n|] ==> transition_idx s T {i,j} < n"
-apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp) 
-apply (simp add: transition_idx_def, blast intro: Least_le) 
+apply (subgoal_tac "transition_idx s T {i, j} \<le> k", simp)
+apply (simp add: transition_idx_def, blast intro: Least_le)
 done
 
 lemma transition_idx_in:
     "[|i<j; (s j, s i) \<in> T k|] ==> (s j, s i) \<in> T (transition_idx s T {i,j})"
-apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR 
-            cong: conj_cong) 
-apply (erule LeastI) 
+apply (simp add: transition_idx_def doubleton_eq_iff conj_disj_distribR
+            cong: conj_cong)
+apply (erule LeastI)
 done
 
 text{*To be equal to the union of some well-founded relations is equivalent
 to being the subset of such a union.*}
 lemma disj_wf:
      "disj_wf(r) = (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) & r \<subseteq> (\<Union>i<n. T i))"
-apply (auto simp add: disj_wf_def) 
-apply (rule_tac x="%i. T i Int r" in exI) 
-apply (rule_tac x=n in exI) 
-apply (force simp add: wf_Int1) 
+apply (auto simp add: disj_wf_def)
+apply (rule_tac x="%i. T i Int r" in exI)
+apply (rule_tac x=n in exI)
+apply (force simp add: wf_Int1)
 done
 
 theorem trans_disj_wf_implies_wf:
@@ -388,13 +384,13 @@
   proof -
     fix i and j::nat
     assume less: "i<j"
-    thus "(s j, s i) \<in> r"
+    then show "(s j, s i) \<in> r"
     proof (rule less_Suc_induct)
-      show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc) 
+      show "\<And>i. (s (Suc i), s i) \<in> r" by (simp add: sSuc)
       show "\<And>i j k. \<lbrakk>(s j, s i) \<in> r; (s k, s j) \<in> r\<rbrakk> \<Longrightarrow> (s k, s i) \<in> r"
-        using transr by (unfold trans_def, blast) 
+        using transr by (unfold trans_def, blast)
     qed
-  qed    
+  qed
   from dwf
   obtain T and n::nat where wfT: "\<forall>k<n. wf(T k)" and r: "r = (\<Union>k<n. T k)"
     by (auto simp add: disj_wf_def)
@@ -402,20 +398,20 @@
   proof -
     fix i and j::nat
     assume less: "i<j"
-    hence "(s j, s i) \<in> r" by (rule s [of i j]) 
-    thus "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
-  qed    
+    then have "(s j, s i) \<in> r" by (rule s [of i j])
+    then show "\<exists>k. (s j, s i) \<in> T k & k<n" by (auto simp add: r)
+  qed
   have trless: "!!i j. i\<noteq>j ==> transition_idx s T {i,j} < n"
     apply (auto simp add: linorder_neq_iff)
-    apply (blast dest: s_in_T transition_idx_less) 
-    apply (subst insert_commute)   
-    apply (blast dest: s_in_T transition_idx_less) 
+    apply (blast dest: s_in_T transition_idx_less)
+    apply (subst insert_commute)
+    apply (blast dest: s_in_T transition_idx_less)
     done
   have
-   "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n & 
+   "\<exists>K k. K \<subseteq> UNIV & infinite K & k < n &
           (\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k)"
-    by (rule Ramsey2) (auto intro: trless nat_infinite) 
-  then obtain K and k 
+    by (rule Ramsey2) (auto intro: trless nat_infinite)
+  then obtain K and k
     where infK: "infinite K" and less: "k < n" and
           allk: "\<forall>i\<in>K. \<forall>j\<in>K. i\<noteq>j --> transition_idx s T {i,j} = k"
     by auto
@@ -424,18 +420,18 @@
     fix m::nat
     let ?j = "enumerate K (Suc m)"
     let ?i = "enumerate K m"
-    have jK: "?j \<in> K" by (simp add: enumerate_in_set infK) 
-    have iK: "?i \<in> K" by (simp add: enumerate_in_set infK) 
-    have ij: "?i < ?j" by (simp add: enumerate_step infK) 
-    have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij 
+    have jK: "?j \<in> K" by (simp add: enumerate_in_set infK)
+    have iK: "?i \<in> K" by (simp add: enumerate_in_set infK)
+    have ij: "?i < ?j" by (simp add: enumerate_step infK)
+    have ijk: "transition_idx s T {?i,?j} = k" using iK jK ij
       by (simp add: allk)
-    obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n" 
+    obtain k' where "(s ?j, s ?i) \<in> T k'" "k'<n"
       using s_in_T [OF ij] by blast
-    thus "(s ?j, s ?i) \<in> T k" 
-      by (simp add: ijk [symmetric] transition_idx_in ij) 
+    then show "(s ?j, s ?i) \<in> T k"
+      by (simp add: ijk [symmetric] transition_idx_in ij)
   qed
-  hence "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain) 
-  thus False using wfT less by blast
+  then have "~ wf(T k)" by (force simp add: wf_iff_no_infinite_down_chain)
+  then show False using wfT less by blast
 qed
 
 end
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -537,8 +537,6 @@
 declare ask_inv_client_map_drop_map [simp]
 
 
-declare finite_lessThan [iff]
-
 text{*Client : <unfolded specification> *}
 lemmas client_spec_simps =
   client_spec_def client_increasing_def client_bounded_def
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/Comp/Progress.thy
--- a/src/HOL/UNITY/Comp/Progress.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Comp/Progress.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -13,10 +13,10 @@
 text{*Thesis Section 4.4.2*}
 
 definition FF :: "int program" where
-    "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
+    "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
 
 definition GG :: "int program" where
-    "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
+    "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
 
 subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
 
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/ELT.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -166,7 +166,7 @@
 apply (erule leadsETo_induct)
 prefer 3 apply (blast intro: leadsETo_Union)
 prefer 2 apply (blast intro: leadsETo_Trans)
-apply (blast intro: leadsETo_Basis)
+apply blast
 done
 
 lemma leadsETo_Trans_Un:
@@ -237,7 +237,7 @@
 lemma leadsETo_givenBy:
      "[| F : A leadsTo[CC] A';  CC <= givenBy v |]  
       ==> F : A leadsTo[givenBy v] A'"
-by (blast intro: empty_mem_givenBy leadsETo_weaken)
+by (blast intro: leadsETo_weaken)
 
 
 (*Set difference*)
@@ -340,7 +340,7 @@
  apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
 apply (rule leadsETo_Basis)
 apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] 
-                      Int_Diff ensures_def givenBy_eq_Collect Join_transient)
+                      Int_Diff ensures_def givenBy_eq_Collect)
 prefer 3 apply (blast intro: transient_strengthen)
 apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
 apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
@@ -454,7 +454,7 @@
 lemma lel_lemma:
      "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B"
 apply (erule leadsTo_induct)
-  apply (blast intro: reachable_ensures leadsETo_Basis)
+  apply (blast intro: reachable_ensures)
  apply (blast dest: e_psp_stable2 intro: leadsETo_Trans leadsETo_weaken_L)
 apply (subst Int_Union)
 apply (blast intro: leadsETo_UN)
@@ -491,7 +491,7 @@
       ==> extend h F : (extend_set h A) leadsTo[extend_set h ` CC]  
                        (extend_set h B)"
 apply (erule leadsETo_induct)
-  apply (force intro: leadsETo_Basis subset_imp_ensures 
+  apply (force intro: subset_imp_ensures 
                simp add: extend_ensures extend_set_Diff_distrib [symmetric])
  apply (blast intro: leadsETo_Trans)
 apply (simp add: leadsETo_UN extend_set_Union)
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Extend.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -370,9 +370,7 @@
 
 lemma (in Extend) Allowed_extend:
      "Allowed (extend h F) = project h UNIV -` Allowed F"
-apply (simp (no_asm) add: AllowedActs_extend Allowed_def)
-apply blast
-done
+by (auto simp add: Allowed_def)
 
 lemma (in Extend) extend_SKIP [simp]: "extend h SKIP = SKIP"
 apply (unfold SKIP_def)
@@ -634,7 +632,7 @@
      "extend h F \<in> AU leadsTo BU  
       ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
 apply (erule leadsTo_induct)
-  apply (blast intro: extend_ensures_slice leadsTo_Basis)
+  apply (blast intro: extend_ensures_slice)
  apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
 apply (simp add: leadsTo_UN slice_Union)
 done
@@ -682,7 +680,7 @@
      "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
 apply (rule program_equalityI)
   apply (simp add: project_set_extend_set_Int)
- apply (simp add: image_eq_UN UN_Un, auto)
+ apply (auto simp add: image_eq_UN)
 done
 
 lemma (in Extend) extend_Join_eq_extend_D:
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Guar.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -17,7 +17,7 @@
 begin
 
 instance program :: (type) order
-proof qed (auto simp add: program_less_le dest: component_antisym intro: component_refl component_trans)
+  by default (auto simp add: program_less_le dest: component_antisym intro: component_trans)
 
 text{*Existential and Universal properties.  I formalize the two-program
       case, proving equivalence with Chandy and Sanders's n-ary definitions*}
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -120,7 +120,7 @@
        else if i<j then insert_map j t (f(i:=s))  
        else insert_map j t (f(i - Suc 0 := s)))"
 apply (rule ext) 
-apply (simp split add: nat_diff_split) 
+apply (simp split add: nat_diff_split)
  txt{*This simplification is VERY slow*}
 done
 
@@ -254,7 +254,7 @@
 lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
 apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
 apply (simp add: lift_def rename_preserves)
-apply (simp add: lift_map_def o_def split_def del: split_comp_eq)
+apply (simp add: lift_map_def o_def split_def)
 done
 
 lemma delete_map_eqE':
@@ -327,9 +327,9 @@
       ==> lift i F \<in> preserves (v o sub j o fst) =  
           (if i=j then F \<in> preserves (v o fst) else True)"
 apply (drule subset_preserves_o [THEN subsetD])
-apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
+apply (simp add: lift_preserves_eq o_def)
 apply (auto cong del: if_weak_cong 
-       simp add: lift_map_def eq_commute split_def o_def simp del:split_comp_eq)
+       simp add: lift_map_def eq_commute split_def o_def)
 done
 
 
@@ -409,10 +409,10 @@
 by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
 
 lemma Allowed_lift [simp]: "Allowed (lift i F) = lift i ` (Allowed F)"
-by (simp add: lift_def Allowed_rename)
+by (simp add: lift_def)
 
 lemma lift_image_preserves:
      "lift i ` preserves v = preserves (v o drop_map i)"
-by (simp add: rename_image_preserves lift_def inv_lift_map_eq)
+by (simp add: rename_image_preserves lift_def)
 
 end
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/ListOrder.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -208,7 +208,7 @@
      "[| refl r;  (xs,ys) : genPrefix r;  length xs = length ys |]  
       ==>  (xs@zs, ys @ zs) : genPrefix r"
 apply (drule genPrefix_take_append, assumption)
-apply (simp add: take_all)
+apply simp
 done
 
 
@@ -301,14 +301,10 @@
 (** recursion equations **)
 
 lemma Nil_prefix [iff]: "[] <= xs"
-apply (unfold prefix_def)
-apply (simp add: Nil_genPrefix)
-done
+by (simp add: prefix_def)
 
 lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])"
-apply (unfold prefix_def)
-apply (simp add: genPrefix_Nil)
-done
+by (simp add: prefix_def)
 
 lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)"
 by (simp add: prefix_def)
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/PPROD.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -29,7 +29,7 @@
 by (simp add: PLam_def)
 
 lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
-by (simp add: PLam_def lift_SKIP JN_constant)
+by (simp add: PLam_def JN_constant)
 
 lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
 by (unfold PLam_def, auto)
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/Rename.thy
--- a/src/HOL/UNITY/Rename.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Rename.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -64,7 +64,7 @@
 apply (simp add: bij_extend_act_eq_project_act)
 apply (rule surjI)
 apply (rule Extend.extend_act_inverse)
-apply (blast intro: bij_imp_bij_inv good_map_bij)
+apply (blast intro: bij_imp_bij_inv)
 done
 
 lemma bij_project_act: "bij h ==> bij (project_act (%(x,u::'c). h x))"
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/UNITY.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -58,9 +58,6 @@
     "increasing f == \<Inter>z. stable {s. z \<le> f s}"
 
 
-text{*Perhaps HOL shouldn't add this in the first place!*}
-declare image_Collect [simp del]
-
 subsubsection{*The abstract type of programs*}
 
 lemmas program_typedef =
@@ -73,7 +70,7 @@
 done
 
 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
-by (simp add: insert_absorb Id_in_Acts)
+by (simp add: insert_absorb)
 
 lemma Acts_nonempty [simp]: "Acts F \<noteq> {}"
 by auto
@@ -84,7 +81,7 @@
 done
 
 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
-by (simp add: insert_absorb Id_in_AllowedActs)
+by (simp add: insert_absorb)
 
 subsubsection{*Inspectors for type "program"*}
 
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/HOL/UNITY/Union.thy	Tue Feb 21 17:09:53 2012 +0100
@@ -202,7 +202,7 @@
 
 lemma Join_unless [simp]:
      "(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
-by (simp add: Join_constrains unless_def)
+by (simp add: unless_def)
 
 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
   reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
@@ -238,12 +238,12 @@
 lemma Join_increasing [simp]:
      "(F\<squnion>G \<in> increasing f) =  
       (F \<in> increasing f & G \<in> increasing f)"
-by (simp add: increasing_def Join_stable, blast)
+by (auto simp add: increasing_def)
 
 lemma invariant_JoinI:
      "[| F \<in> invariant A; G \<in> invariant A |]   
       ==> F\<squnion>G \<in> invariant A"
-by (simp add: invariant_def, blast)
+by (auto simp add: invariant_def)
 
 lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
 by (simp add: FP_def JN_stable INTER_eq)
@@ -262,10 +262,10 @@
 by (auto simp add: bex_Un transient_def Join_def)
 
 lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A"
-by (simp add: Join_transient)
+by simp
 
 lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
-by (simp add: Join_transient)
+by simp
 
 (*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
 lemma JN_ensures:
@@ -278,7 +278,7 @@
      "F\<squnion>G \<in> A ensures B =      
       (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &  
        (F \<in> transient (A-B) | G \<in> transient (A-B)))"
-by (auto simp add: ensures_def Join_transient)
+by (auto simp add: ensures_def)
 
 lemma stable_Join_constrains: 
     "[| F \<in> stable A;  G \<in> A co A' |]  
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Pure/PIDE/text.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -74,6 +74,8 @@
   {
     val empty: Perspective = Perspective(Nil)
 
+    def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2)))
+
     def apply(ranges: Seq[Range]): Perspective =
     {
       val result = new mutable.ListBuffer[Text.Range]
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Pure/System/session.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -216,7 +216,7 @@
 
     /* delayed command changes */
 
-    object commands_changed_delay
+    object delay_commands_changed
     {
       private var changed_nodes: Set[Document.Node.Name] = Set.empty
       private var changed_commands: Set[Command] = Set.empty
@@ -299,7 +299,7 @@
     //{{{
     {
       val cmds = global_state.change_yield(_.assign(id, assign))
-      for (cmd <- cmds) commands_changed_delay.invoke(cmd)
+      for (cmd <- cmds) delay_commands_changed.invoke(cmd)
     }
     //}}}
 
@@ -359,7 +359,7 @@
         case Position.Id(state_id) if !result.is_raw =>
           try {
             val st = global_state.change_yield(_.accumulate(state_id, result.message))
-            commands_changed_delay.invoke(st.command)
+            delay_commands_changed.invoke(st.command)
           }
           catch {
             case _: Document.State.Fail => bad_result(result)
@@ -430,8 +430,8 @@
     //{{{
     var finished = false
     while (!finished) {
-      receiveWithin(commands_changed_delay.flush_timeout) {
-        case TIMEOUT => commands_changed_delay.flush()
+      receiveWithin(delay_commands_changed.flush_timeout) {
+        case TIMEOUT => delay_commands_changed.flush()
 
         case Start(timeout, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/Pure/System/swing_thread.scala
--- a/src/Pure/System/swing_thread.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Pure/System/swing_thread.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -53,7 +53,7 @@
     val timer = new Timer(time.ms.toInt, listener)
     timer.setRepeats(false)
 
-    def invoke() { now { if (first) timer.start() else timer.restart() } }
+    def invoke() { later { if (first) timer.start() else timer.restart() } }
     invoke _
   }
 
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Feb 21 17:09:53 2012 +0100
@@ -25,6 +25,7 @@
   "src/scala_console.scala"
   "src/session_dockable.scala"
   "src/text_area_painter.scala"
+  "src/text_overview.scala"
   "src/token_markup.scala"
 )
 
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -10,17 +10,16 @@
 
 import isabelle._
 
-import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.collection.immutable.SortedMap
 import scala.actors.Actor._
 
 import java.lang.System
 import java.text.BreakIterator
-import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
-import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
+import java.awt.{Color, Graphics2D, Point}
+import java.awt.event.{MouseMotionAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
-import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
+import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
 import javax.swing.event.{CaretListener, CaretEvent}
 
 import org.gjt.sp.util.Log
@@ -348,83 +347,12 @@
   }
 
 
-  /* overview of command status left of scrollbar */
-
-  private val overview = new JPanel(new BorderLayout)
-  {
-    private val WIDTH = 10
-    private val HEIGHT = 2
-
-    private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines
-
-    setPreferredSize(new Dimension(WIDTH, 0))
-
-    setRequestFocusEnabled(false)
-
-    addMouseListener(new MouseAdapter {
-      override def mousePressed(event: MouseEvent) {
-        val line = (event.getY * lines()) / getHeight
-        if (line >= 0 && line < text_area.getLineCount)
-          text_area.setCaretPosition(text_area.getLineStartOffset(line))
-      }
-    })
-
-    override def addNotify() {
-      super.addNotify()
-      ToolTipManager.sharedInstance.registerComponent(this)
-    }
-
-    override def removeNotify() {
-      ToolTipManager.sharedInstance.unregisterComponent(this)
-      super.removeNotify
-    }
-
-    override def paintComponent(gfx: Graphics)
-    {
-      super.paintComponent(gfx)
-      Swing_Thread.assert()
+  /* text status overview left of scrollbar */
 
-      robust_body(()) {
-        val buffer = model.buffer
-        Isabelle.buffer_lock(buffer) {
-          val snapshot = update_snapshot()
-
-          gfx.setColor(getBackground)
-          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
-
-          val line_count = buffer.getLineCount
-          val char_count = buffer.getLength
-
-          val L = lines()
-          val H = getHeight()
-
-          @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
-          {
-            if (l < line_count && h < H) {
-              val p1 = p + H
-              val q1 = q + HEIGHT * L
-              val (l1, h1) =
-                if (p1 >= q1) (l + 1, h + (p1 - q) / L)
-                else (l + (q1 - p) / H, h + HEIGHT)
-
-              val start = buffer.getLineStartOffset(l)
-              val end =
-                if (l1 < line_count) buffer.getLineStartOffset(l1)
-                else char_count
-
-              Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
-                case None =>
-                case Some(color) =>
-                  gfx.setColor(color)
-                  gfx.fillRect(0, h, getWidth, h1 - h)
-              }
-              paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
-            }
-          }
-          paint_loop(0, 0, 0, 0)
-        }
-      }
-    }
+  private val overview = new Text_Overview(this)
+  {
+    val delay_repaint =
+      Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
   }
 
 
@@ -442,7 +370,7 @@
             if (updated ||
                 (changed.nodes.contains(model.name) &&
                  changed.commands.exists(snapshot.node.commands.contains)))
-              overview.repaint()
+              overview.delay_repaint()
 
             if (updated) invalidate_range(visible)
             else {
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Feb 21 13:19:16 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -132,7 +132,7 @@
   /* resize */
 
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
+    val delay = Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
     override def componentResized(e: ComponentEvent) { delay() }
   })
 
diff -r 1152f98902e7 -r 1bc7e91a5c77 src/Tools/jEdit/src/text_overview.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/text_overview.scala	Tue Feb 21 17:09:53 2012 +0100
@@ -0,0 +1,97 @@
+/*  Title:      Tools/jEdit/src/text_overview.scala
+    Author:     Makarius
+
+Swing component for text status overview.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.annotation.tailrec
+
+import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension}
+import java.awt.event.{MouseAdapter, MouseEvent}
+import javax.swing.{JPanel, ToolTipManager}
+
+
+class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout)
+{
+  private val text_area = doc_view.text_area
+  private val buffer = doc_view.model.buffer
+
+  private val WIDTH = 10
+  private val HEIGHT = 2
+
+  private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
+
+  setPreferredSize(new Dimension(WIDTH, 0))
+
+  setRequestFocusEnabled(false)
+
+  addMouseListener(new MouseAdapter {
+    override def mousePressed(event: MouseEvent) {
+      val line = (event.getY * lines()) / getHeight
+      if (line >= 0 && line < text_area.getLineCount)
+        text_area.setCaretPosition(text_area.getLineStartOffset(line))
+    }
+  })
+
+  override def addNotify() {
+    super.addNotify()
+    ToolTipManager.sharedInstance.registerComponent(this)
+  }
+
+  override def removeNotify() {
+    ToolTipManager.sharedInstance.unregisterComponent(this)
+    super.removeNotify
+  }
+
+  override def paintComponent(gfx: Graphics)
+  {
+    super.paintComponent(gfx)
+    Swing_Thread.assert()
+
+    doc_view.robust_body(()) {
+      Isabelle.buffer_lock(buffer) {
+        val snapshot = doc_view.update_snapshot()
+
+        gfx.setColor(getBackground)
+        gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+
+        val line_count = buffer.getLineCount
+        val char_count = buffer.getLength
+
+        val L = lines()
+        val H = getHeight()
+
+        @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
+        {
+          if (l < line_count && h < H) {
+            val p1 = p + H
+            val q1 = q + HEIGHT * L
+            val (l1, h1) =
+              if (p1 >= q1) (l + 1, h + (p1 - q) / L)
+              else (l + (q1 - p) / H, h + HEIGHT)
+
+            val start = buffer.getLineStartOffset(l)
+            val end =
+              if (l1 < line_count) buffer.getLineStartOffset(l1)
+              else char_count
+
+            Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
+              case None =>
+              case Some(color) =>
+                gfx.setColor(color)
+                gfx.fillRect(0, h, getWidth, h1 - h)
+            }
+            paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
+          }
+        }
+        paint_loop(0, 0, 0, 0)
+      }
+    }
+  }
+}
+