--- a/NEWS Mon Jul 11 22:02:18 2016 +0200
+++ b/NEWS Mon Jul 11 22:07:02 2016 +0200
@@ -149,6 +149,9 @@
*** HOL ***
+* Theory Set_Interval.thy: substantial new theorems on indexed sums
+and products.
+
* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying
equations in functional programming style: variables present on the
left-hand but not on the righ-hand side are replaced by underscores.
--- a/src/HOL/Data_Structures/Cmp.thy Mon Jul 11 22:02:18 2016 +0200
+++ b/src/HOL/Data_Structures/Cmp.thy Mon Jul 11 22:07:02 2016 +0200
@@ -8,18 +8,14 @@
datatype cmp_val = LT | EQ | GT
-function cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where
-"x < y \<Longrightarrow> cmp x y = LT" |
-"x = y \<Longrightarrow> cmp x y = EQ" |
-"x > y \<Longrightarrow> cmp x y = GT"
-by (auto, force)
-termination by lexicographic_order
+definition cmp :: "'a:: linorder \<Rightarrow> 'a \<Rightarrow> cmp_val" where
+"cmp x y = (if x < y then LT else if x=y then EQ else GT)"
lemma
LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
and EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
and GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
-by (cases x y rule: linorder_cases, auto)+
+by (auto simp: cmp_def)
lemma case_cmp_if[simp]: "(case c of EQ \<Rightarrow> e | LT \<Rightarrow> l | GT \<Rightarrow> g) =
(if c = LT then l else if c = GT then g else e)"