# HG changeset patch
# User traytel
# Date 1361561151 -3600
# Node ID 5013ed756a787678aadd7b2eff316f6da094f482
# Parent  029de23bb5e8117cb38a55ee525477ab546724b8# Parent  311fe56541eae4652381b14fdd04e79f85bab01a
merged

diff -r 029de23bb5e8 -r 5013ed756a78 NEWS
--- a/NEWS	Fri Feb 22 13:39:47 2013 +0100
+++ b/NEWS	Fri Feb 22 20:25:51 2013 +0100
@@ -6,6 +6,9 @@
 
 *** HOL ***
 
+* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
+Isabelle2013).  Use "isabelle build" to operate on Isabelle sessions.
+
 * Numeric types mapped by default to target language numerals:
 natural (replaces former code_numeral) and integer (replaces
 former code_int).  Conversions are available as integer_of_natural /
diff -r 029de23bb5e8 -r 5013ed756a78 src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Feb 22 20:25:51 2013 +0100
@@ -6,42 +6,83 @@
 
 subsection "Interval Analysis"
 
-datatype ivl = Ivl "int option" "int option"
+datatype lb = Minf | Lb int
+datatype ub = Pinf | Ub int
+
+datatype ivl = Ivl lb ub
 
 definition "\<gamma>_ivl i = (case i of
-  Ivl (Some l) (Some h) \<Rightarrow> {l..h} |
-  Ivl (Some l) None \<Rightarrow> {l..} |
-  Ivl None (Some h) \<Rightarrow> {..h} |
-  Ivl None None \<Rightarrow> UNIV)"
+  Ivl (Lb l) (Ub h) \<Rightarrow> {l..h} |
+  Ivl (Lb l) Pinf \<Rightarrow> {l..} |
+  Ivl Minf (Ub h) \<Rightarrow> {..h} |
+  Ivl Minf Pinf \<Rightarrow> UNIV)"
 
-abbreviation Ivl_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
-"{lo\<dots>hi} == Ivl (Some lo) (Some hi)"
-abbreviation Ivl_Some_None :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
-"{lo\<dots>} == Ivl (Some lo) None"
-abbreviation Ivl_None_Some :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
-"{\<dots>hi} == Ivl None (Some hi)"
-abbreviation Ivl_None_None :: "ivl"  ("{\<dots>}") where
-"{\<dots>} == Ivl None None"
+abbreviation Ivl_Lb_Ub :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
+"{lo\<dots>hi} == Ivl (Lb lo) (Ub hi)"
+abbreviation Ivl_Lb_Pinf :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
+"{lo\<dots>} == Ivl (Lb lo) Pinf"
+abbreviation Ivl_Minf_Ub :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
+"{\<dots>hi} == Ivl Minf (Ub hi)"
+abbreviation Ivl_Minf_Pinf :: "ivl"  ("{\<dots>}") where
+"{\<dots>} == Ivl Minf Pinf"
+
+lemmas lub_splits = lb.splits ub.splits
 
 definition "num_ivl n = {n\<dots>n}"
 
 fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where
-"in_ivl k (Ivl (Some l) (Some h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
-"in_ivl k (Ivl (Some l) None) \<longleftrightarrow> l \<le> k" |
-"in_ivl k (Ivl None (Some h)) \<longleftrightarrow> k \<le> h" |
-"in_ivl k (Ivl None None) \<longleftrightarrow> True"
+"in_ivl k (Ivl (Lb l) (Ub h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
+"in_ivl k (Ivl (Lb l) Pinf) \<longleftrightarrow> l \<le> k" |
+"in_ivl k (Ivl Minf (Ub h)) \<longleftrightarrow> k \<le> h" |
+"in_ivl k (Ivl Minf Pinf) \<longleftrightarrow> True"
 
-instantiation option :: (plus)plus
+
+instantiation lb :: order
 begin
 
-fun plus_option where
-"Some x + Some y = Some(x+y)" |
-"_ + _ = None"
+definition less_eq_lb where
+"l1 \<le> l2 = (case l1 of Minf \<Rightarrow> True | Lb i1 \<Rightarrow> (case l2 of Minf \<Rightarrow> False | Lb i2 \<Rightarrow> i1 \<le> i2))"
+
+definition less_lb :: "lb \<Rightarrow> lb \<Rightarrow> bool" where
+"((l1::lb) < l2) = (l1 \<le> l2 & ~ l1 \<ge> l2)"
 
-instance ..
+instance
+proof
+  case goal1 show ?case by(rule less_lb_def)
+next
+  case goal2 show ?case by(auto simp: less_eq_lb_def split:lub_splits)
+next
+  case goal3 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
+next
+  case goal4 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
+qed
 
 end
 
+instantiation ub :: order
+begin
+
+definition less_eq_ub where
+"u1 \<le> u2 = (case u2 of Pinf \<Rightarrow> True | Ub i2 \<Rightarrow> (case u1 of Pinf \<Rightarrow> False | Ub i1 \<Rightarrow> i1 \<le> i2))"
+
+definition less_ub :: "ub \<Rightarrow> ub \<Rightarrow> bool" where
+"((u1::ub) < u2) = (u1 \<le> u2 & ~ u1 \<ge> u2)"
+
+instance
+proof
+  case goal1 show ?case by(rule less_ub_def)
+next
+  case goal2 show ?case by(auto simp: less_eq_ub_def split:lub_splits)
+next
+  case goal3 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
+next
+  case goal4 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
+qed
+
+end
+
+lemmas le_lub_defs = less_eq_lb_def less_eq_ub_def
+
 definition empty where "empty = {1\<dots>0}"
 
 fun is_empty where
@@ -49,63 +90,49 @@
 "is_empty _ = False"
 
 lemma [simp]: "is_empty(Ivl l h) =
-  (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
-by(auto split:option.split)
+  (case l of Lb l \<Rightarrow> (case h of Ub h \<Rightarrow> h<l | Pinf \<Rightarrow> False) | Minf \<Rightarrow> False)"
+by(auto split: lub_splits)
 
 lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
-by(auto simp add: \<gamma>_ivl_def split: ivl.split option.split)
+by(auto simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
 
-definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
-  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1+l2) (h1+h2))"
 
 instantiation ivl :: semilattice
 begin
 
-definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
-"le_option pos x y =
- (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
-  | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
-
 fun le_aux where
-"le_aux (Ivl l1 h1) (Ivl l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
+"le_aux (Ivl l1 h1) (Ivl l2 h2) = (l2 \<le> l1 & h1 \<le> h2)"
 
 definition le_ivl where
 "i1 \<sqsubseteq> i2 =
  (if is_empty i1 then True else
   if is_empty i2 then False else le_aux i1 i2)"
 
-definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
-"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
-
-definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
-"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
-
 definition "i1 \<squnion> i2 =
  (if is_empty i1 then i2 else if is_empty i2 then i1
-  else case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
-          Ivl (min_option False l1 l2) (max_option True h1 h2))"
+  else case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (min l1 l2) (max h1 h2))"
 
 definition "\<top> = {\<dots>}"
 
 instance
 proof
   case goal1 thus ?case
-    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
+    by(cases x, simp add: le_ivl_def)
 next
   case goal2 thus ?case
-    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
+    by(cases x, cases y, cases z, auto simp: le_ivl_def split: if_splits)
 next
   case goal3 thus ?case
-    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
 next
   case goal4 thus ?case
-    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
 next
   case goal5 thus ?case
-    by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits)
+    by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits if_splits)
 next
   case goal6 thus ?case
-    by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
+    by(cases x, simp add: Top_ivl_def le_ivl_def le_lub_defs split: lub_splits)
 qed
 
 end
@@ -115,108 +142,150 @@
 begin
 
 definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
-  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
-    Ivl (max_option False l1 l2) (min_option True h1 h2))"
+  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (max l1 l2) (min h1 h2))"
 
 definition "\<bottom> = empty"
 
 instance
 proof
   case goal2 thus ?case
-    by (simp add:meet_ivl_def empty_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+    by (simp add:meet_ivl_def empty_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
 next
   case goal3 thus ?case
-    by (simp add: empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
+    by (simp add: empty_def meet_ivl_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
 next
   case goal4 thus ?case
-    by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
+    by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_lub_defs max_def min_def split: lub_splits if_splits)
 next
   case goal1 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
 qed
 
 end
 
-instantiation option :: (minus)minus
+
+instantiation lb :: plus
 begin
 
-fun minus_option where
-"Some x - Some y = Some(x-y)" |
-"_ - _ = None"
+fun plus_lb where
+"Lb x + Lb y = Lb(x+y)" |
+"_ + _ = Minf"
+
+instance ..
+end
+
+instantiation ub :: plus
+begin
+
+fun plus_ub where
+"Ub x + Ub y = Ub(x+y)" |
+"_ + _ = Pinf"
+
+instance ..
+end
+
+instantiation ivl :: plus
+begin
+
+definition "i1+i2 = (if is_empty i1 | is_empty i2 then empty else
+  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1+l2) (h1+h2))"
 
 instance ..
+end
 
+fun uminus_ub :: "ub \<Rightarrow> lb" where
+"uminus_ub(Ub( x)) = Lb(-x)" |
+"uminus_ub Pinf = Minf"
+
+fun uminus_lb :: "lb \<Rightarrow> ub" where
+"uminus_lb(Lb( x)) = Ub(-x)" |
+"uminus_lb Minf = Pinf"
+
+instantiation ivl :: minus
+begin
+
+definition "i1 - i2 = (if is_empty i1 | is_empty i2 then empty else
+  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1 + uminus_ub h2) (h1 + uminus_lb l2))"
+
+instance ..
 end
 
-definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
-  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1-h2) (h1-l2))"
+instantiation ivl :: uminus
+begin
+
+fun uminus_ivl where
+"-(Ivl l h) = Ivl (uminus_ub h) (uminus_lb l)"
+
+instance ..
+end
+
+lemma minus_ivl_nice_def: "(i1::ivl) - i2 = i1 + -i2"
+by(auto simp: plus_ivl_def minus_ivl_def split: ivl.split lub_splits)
 
 lemma gamma_minus_ivl:
-  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)"
-by(auto simp add: minus_ivl_def \<gamma>_ivl_def split: ivl.splits option.splits)
+  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(i1 - i2)"
+by(auto simp add: minus_ivl_def \<gamma>_ivl_def split: ivl.splits lub_splits)
 
 definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
-  i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
+  i1 \<sqinter> (i - i2), i2 \<sqinter> (i - i1))"
 
 fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
 "filter_less_ivl res (Ivl l1 h1) (Ivl l2 h2) =
   (if is_empty(Ivl l1 h1) \<or> is_empty(Ivl l2 h2) then (empty, empty) else
    if res
-   then (Ivl l1 (min_option True h1 (h2 - Some 1)),
-         Ivl (max_option False (l1 + Some 1) l2) h2)
-   else (Ivl (max_option False l1 l2) h1, Ivl l2 (min_option True h1 h2)))"
+   then (Ivl l1 (min h1 (h2 + Ub -1)), Ivl (max (l1 + Lb 1) l2) h2)
+   else (Ivl (max l1 l2) h1, Ivl l2 (min h1 h2)))"
 
 interpretation Val_abs
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 proof
   case goal1 thus ?case
-    by(auto simp: \<gamma>_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
+    by(auto simp: \<gamma>_ivl_def le_ivl_def le_lub_defs split: ivl.split lub_splits if_splits)
 next
   case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
 next
   case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
 next
   case goal4 thus ?case
-    by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
+    by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split lub_splits)
 qed
 
 interpretation Val_abs1_gamma
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 defines aval_ivl is aval'
 proof
   case goal1 thus ?case
-    by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
+    by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_def max_def split: ivl.split lub_splits)
 next
   case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def)
 qed
 
-lemma mono_minus_ivl:
-  "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> minus_ivl i1 i2 \<sqsubseteq> minus_ivl i1' i2'"
-apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_option_def split: ivl.splits)
-  apply(simp split: option.splits)
- apply(simp split: option.splits)
-apply(simp split: option.splits)
+lemma mono_minus_ivl: fixes i1 :: ivl
+shows "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> i1 - i2 \<sqsubseteq> i1' - i2'"
+apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_lub_defs split: ivl.splits)
+  apply(simp split: lub_splits)
+ apply(simp split: lub_splits)
+apply(simp split: lub_splits)
 done
 
 
 interpretation Val_abs1
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 proof
   case goal1 thus ?case
-    by (simp add: \<gamma>_ivl_def split: ivl.split option.split)
+    by (simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
 next
   case goal2 thus ?case
     by(auto simp add: filter_plus_ivl_def)
       (metis gamma_minus_ivl add_diff_cancel add_commute)+
 next
   case goal3 thus ?case
-    by(cases a1, cases a2,
-      auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
+    by(cases a1, cases a2, auto simp: \<gamma>_ivl_def min_def max_def split: if_splits lub_splits)
 qed
 
 interpretation Abs_Int1
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 defines afilter_ivl is afilter
@@ -230,19 +299,19 @@
 text{* Monotonicity: *}
 
 interpretation Abs_Int1_mono
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 proof
   case goal1 thus ?case
-    by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits option.splits)
+    by(auto simp: plus_ivl_def le_ivl_def le_lub_defs empty_def split: if_splits ivl.splits lub_splits)
 next
   case goal2 thus ?case
     by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
 next
   case goal3 thus ?case
     apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
-    by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
+    by(auto simp add: empty_def le_ivl_def le_lub_defs min_def max_def split: lub_splits)
 qed
 
 
diff -r 029de23bb5e8 -r 5013ed756a78 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Fri Feb 22 20:25:51 2013 +0100
@@ -87,18 +87,18 @@
   ((*if is_empty ivl1 then ivl2 else
    if is_empty ivl2 then ivl1 else*)
      case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
-       Ivl (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
-           (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
+       Ivl (if l2 \<le> l1 \<and> l2 \<noteq> l1 then Minf else l1)
+           (if h1 \<le> h2 \<and> h1 \<noteq> h2 then Pinf else h1))"
 
 definition "narrow_ivl ivl1 ivl2 =
   ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
      case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
-       Ivl (if l1 = None then l2 else l1)
-           (if h1 = None then h2 else h1))"
+       Ivl (if l1 = Minf then l2 else l1)
+           (if h1 = Pinf then h2 else h1))"
 
 instance
 proof qed
-  (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
+  (auto simp add: widen_ivl_def narrow_ivl_def le_lub_defs le_ivl_def empty_def split: ivl.split lub_splits if_splits)
 
 end
 
@@ -382,7 +382,7 @@
 end
 
 interpretation Abs_Int2
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 defines AI_ivl' is AI_wn
@@ -583,19 +583,19 @@
 
 definition m_ivl :: "ivl \<Rightarrow> nat" where
 "m_ivl ivl = (case ivl of Ivl l h \<Rightarrow>
-     (case l of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0 | Some _ \<Rightarrow> 1))"
+     (case l of Minf \<Rightarrow> 0 | Lb _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | Ub _ \<Rightarrow> 1))"
 
 lemma m_ivl_height: "m_ivl ivl \<le> 2"
-by(simp add: m_ivl_def split: ivl.split option.split)
+by(simp add: m_ivl_def split: ivl.split lub_splits)
 
 lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
-by(auto simp: m_ivl_def le_option_def le_ivl_def
-        split: ivl.split option.split if_splits)
+by(auto simp: m_ivl_def le_lub_defs le_ivl_def
+        split: ivl.split lub_splits if_splits)
 
 lemma m_ivl_widen:
   "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
-by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def
-        split: ivl.splits option.splits if_splits)
+by(auto simp: m_ivl_def widen_ivl_def le_lub_defs le_ivl_def
+        split: ivl.splits lub_splits if_splits)
 
 definition n_ivl :: "ivl \<Rightarrow> nat" where
 "n_ivl ivl = 2 - m_ivl ivl"
@@ -605,12 +605,12 @@
 
 lemma n_ivl_narrow:
   "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
-by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def
-        split: ivl.splits option.splits if_splits)
+by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_lub_defs le_ivl_def
+        split: ivl.splits lub_splits if_splits)
 
 
 interpretation Abs_Int2_measure
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 and m = m_ivl and n = n_ivl and h = 2
diff -r 029de23bb5e8 -r 5013ed756a78 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Feb 22 13:39:47 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-#
-# approximative IsaMakefile for legacy applications
-#
-
-default: HOL
-
-clean:
-	-@$(ISABELLE_TOOL) build -a -n -c
-
-all:
-	@$(ISABELLE_TOOL) build -a
-
-
-Pure: $(ISABELLE_OUTPUT)/Pure
-
-$(ISABELLE_OUTPUT)/Pure:
-	@$(ISABELLE_TOOL) build -b Pure
-
-
-HOL: $(ISABELLE_OUTPUT)/HOL
-
-$(ISABELLE_OUTPUT)/HOL:
-	@$(ISABELLE_TOOL) build -b HOL
-
-
-HOL-Library: $(ISABELLE_OUTPUT)/HOL-Library
-
-$(ISABELLE_OUTPUT)/HOL-Library:
-	@$(ISABELLE_TOOL) build -b HOL-Library
-
-
-HOL-IMP: $(ISABELLE_OUTPUT)/HOL-IMP
-
-$(ISABELLE_OUTPUT)/HOL-IMP:
-	@$(ISABELLE_TOOL) build -b HOL-IMP
-
-
-HOL-Multivariate_Analysis: $(ISABELLE_OUTPUT)/HOL-Multivariate_Analysis
-
-$(ISABELLE_OUTPUT)/HOL-Multivariate_Analysis:
-	@$(ISABELLE_TOOL) build -b HOL-Multivariate_Analysis
-
-
-HOL-Probability: $(ISABELLE_OUTPUT)/HOL-Probability
-
-$(ISABELLE_OUTPUT)/HOL-Probability:
-	@$(ISABELLE_TOOL) build -b HOL-Probability
-
-
-HOL-Nominal: $(ISABELLE_OUTPUT)/HOL-Nominal
-
-$(ISABELLE_OUTPUT)/HOL-Nominal:
-	@$(ISABELLE_TOOL) build -b HOL-Nominal
-
-
-HOL-Word: $(ISABELLE_OUTPUT)/HOL-Word
-
-$(ISABELLE_OUTPUT)/HOL-Word:
-	@$(ISABELLE_TOOL) build -b HOL-Word
-
-
-HOLCF: $(ISABELLE_OUTPUT)/HOLCF
-
-$(ISABELLE_OUTPUT)/HOLCF:
-	@$(ISABELLE_TOOL) build -b HOLCF
-
diff -r 029de23bb5e8 -r 5013ed756a78 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Fri Feb 22 20:25:51 2013 +0100
@@ -100,8 +100,8 @@
 fun string_of_sequent (gamma, c) =
   string_of_context gamma ^ " \<turnstile> " ^ Atom.string_of c
 
-val string_of_refute_graph =
-  sequents_of_refute_graph #> map string_of_sequent #> cat_lines
+fun string_of_refute_graph refute_graph =
+  refute_graph |> sequents_of_refute_graph |> map string_of_sequent |> cat_lines
 
 fun redirect_sequent tainted bot (gamma, c) =
   if member atom_eq tainted c then
diff -r 029de23bb5e8 -r 5013ed756a78 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Feb 22 20:25:51 2013 +0100
@@ -8,7 +8,7 @@
 
 signature SLEDGEHAMMER_PROOF =
 sig
-	type label = string * int
+  type label = string * int
   type facts = label list * string list
 
   datatype isar_qualifier = Show | Then
diff -r 029de23bb5e8 -r 5013ed756a78 src/HOL/ex/Reflection_Examples.thy
--- a/src/HOL/ex/Reflection_Examples.thy	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/HOL/ex/Reflection_Examples.thy	Fri Feb 22 20:25:51 2013 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Reflection_Ex.thy
+(*  Title:      HOL/ex/Reflection_Examples.thy
     Author:     Amine Chaieb, TU Muenchen
 *)
 
diff -r 029de23bb5e8 -r 5013ed756a78 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/Pure/Isar/runtime.ML	Fri Feb 22 20:25:51 2013 +0100
@@ -52,7 +52,8 @@
   let
     val exn' = Par_Exn.identify [] exn;
     val exec_id = Properties.get (Exn_Properties.get exn') Markup.exec_idN;
-  in ((Par_Exn.the_serial exn', exn'), exec_id) end;
+    val i = Par_Exn.the_serial exn' handle Option.Option => serial ();
+  in ((i, exn'), exec_id) end;
 
 fun flatten _ (CONTEXT (ctxt, exn)) = flatten (SOME ctxt) exn
   | flatten context (Exn.EXCEPTIONS exns) = maps (flatten context) exns
diff -r 029de23bb5e8 -r 5013ed756a78 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Feb 22 20:25:51 2013 +0100
@@ -633,7 +633,7 @@
 
 local
 
-fun timing_message tr t =
+fun timing_message tr (t: Timing.timing) =
   if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr))
   then
     (case approximative_id tr of
@@ -721,7 +721,7 @@
         val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
         val pri =
           if estimate = Time.zeroTime then ~1
-	  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
+          else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
 
         val future_proof = Proof.global_future_proof
           (fn prf =>
diff -r 029de23bb5e8 -r 5013ed756a78 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/Pure/Tools/build.scala	Fri Feb 22 20:25:51 2013 +0100
@@ -693,15 +693,22 @@
               case None => (Path.current, "")
             }
         }
+
+      def ignore_error(msg: String): (List[Properties.T], Double) =
+      {
+        java.lang.System.err.println("### Ignoring bad log file: " + path +
+          (if (msg == "") "" else "\n" + msg))
+        (Nil, 0.0)
+      }
+
       try {
         val info = parse_log(false, text)
         val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
         (info.command_timings, session_timing)
       }
       catch {
-        case ERROR(msg) =>
-          java.lang.System.err.println("### Ignoring bad log file: " + path + "\n" + msg)
-        (Nil, 0.0)
+        case ERROR(msg) => ignore_error(msg)
+        case _: XML.XML_Atom | _: XML.XML_Body => ignore_error("")
       }
     }
 
diff -r 029de23bb5e8 -r 5013ed756a78 src/Pure/Tools/ml_statistics.scala
--- a/src/Pure/Tools/ml_statistics.scala	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/Pure/Tools/ml_statistics.scala	Fri Feb 22 20:25:51 2013 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/ML/ml_statistics.ML
+/*  Title:      Pure/Tools/ml_statistics.scala
     Author:     Makarius
 
 ML runtime statistics.
diff -r 029de23bb5e8 -r 5013ed756a78 src/Pure/Tools/task_statistics.scala
--- a/src/Pure/Tools/task_statistics.scala	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/Pure/Tools/task_statistics.scala	Fri Feb 22 20:25:51 2013 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Pure/ML/task_statistics.ML
+/*  Title:      Pure/Tools/task_statistics.scala
     Author:     Makarius
 
 Future task runtime statistics.
diff -r 029de23bb5e8 -r 5013ed756a78 src/Tools/jEdit/src/fold_handling.scala
--- a/src/Tools/jEdit/src/fold_handling.scala	Fri Feb 22 13:39:47 2013 +0100
+++ b/src/Tools/jEdit/src/fold_handling.scala	Fri Feb 22 20:25:51 2013 +0100
@@ -1,4 +1,4 @@
-/*  Title:      Tools/jEdit/src/fold_handler.scala
+/*  Title:      Tools/jEdit/src/fold_handling.scala
     Author:     Makarius
 
 Handling of folds within the text structure.