--- a/src/HOL/Data_Structures/Cmp.thy Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Data_Structures/Cmp.thy Wed Nov 11 18:32:26 2015 +0100
@@ -1,21 +1,21 @@
-(* Author: Tobias Nipkow *)
-
-section {* Three-Way Comparison *}
-
-theory Cmp
-imports Main
-begin
-
-datatype cmp = LT | EQ | GT
-
-class cmp = linorder +
-fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> cmp"
-assumes LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
-assumes EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
-assumes GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
-
-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)"
-by(simp split: cmp.split)
-
-end
+(* Author: Tobias Nipkow *)
+
+section {* Three-Way Comparison *}
+
+theory Cmp
+imports Main
+begin
+
+datatype cmp = LT | EQ | GT
+
+class cmp = linorder +
+fixes cmp :: "'a \<Rightarrow> 'a \<Rightarrow> cmp"
+assumes LT[simp]: "cmp x y = LT \<longleftrightarrow> x < y"
+assumes EQ[simp]: "cmp x y = EQ \<longleftrightarrow> x = y"
+assumes GT[simp]: "cmp x y = GT \<longleftrightarrow> x > y"
+
+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)"
+by(simp split: cmp.split)
+
+end