src/HOL/Library/Option_ord.thy
changeset 26258 20dfaa28e5e5
parent 26241 b7d8c2338585
child 26259 d30f4a509361
     1.1 --- a/src/HOL/Library/Option_ord.thy	Tue Mar 11 23:09:30 2008 +0100
     1.2 +++ b/src/HOL/Library/Option_ord.thy	Wed Mar 12 08:45:51 2008 +0100
     1.3 @@ -18,34 +18,34 @@
     1.4  definition less_option where
     1.5    [code func del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
     1.6  
     1.7 -lemma less_eq_option_None [simp]: "None \<le> (x\<Colon>'a option)"
     1.8 +lemma less_eq_option_None [simp]: "None \<le> x"
     1.9    by (simp add: less_eq_option_def)
    1.10  
    1.11 -lemma less_eq_option_None_code [code]: "None \<le> (x\<Colon>'a option) \<longleftrightarrow> True"
    1.12 +lemma less_eq_option_None_code [code]: "None \<le> x \<longleftrightarrow> True"
    1.13    by simp
    1.14  
    1.15 -lemma less_eq_option_None_is_None: "(x\<Colon>'a option) \<le> None \<Longrightarrow> x = None"
    1.16 +lemma less_eq_option_None_is_None: "x \<le> None \<Longrightarrow> x = None"
    1.17    by (cases x) (simp_all add: less_eq_option_def)
    1.18  
    1.19 -lemma less_eq_option_Some_None [simp, code]: "Some (x\<Colon>'a) \<le> None \<longleftrightarrow> False"
    1.20 +lemma less_eq_option_Some_None [simp, code]: "Some x \<le> None \<longleftrightarrow> False"
    1.21    by (simp add: less_eq_option_def)
    1.22  
    1.23 -lemma less_eq_option_Some [simp, code]: "Some (x\<Colon>'a) \<le> Some y \<longleftrightarrow> x \<le> y"
    1.24 +lemma less_eq_option_Some [simp, code]: "Some x \<le> Some y \<longleftrightarrow> x \<le> y"
    1.25    by (simp add: less_eq_option_def)
    1.26  
    1.27 -lemma less_option_None [simp, code]: "(x\<Colon>'a option) < None \<longleftrightarrow> False"
    1.28 +lemma less_option_None [simp, code]: "x < None \<longleftrightarrow> False"
    1.29    by (simp add: less_option_def)
    1.30  
    1.31 -lemma less_option_None_is_Some: "None < (x\<Colon>'a option) \<Longrightarrow> \<exists>z. x = Some z"
    1.32 +lemma less_option_None_is_Some: "None < x \<Longrightarrow> \<exists>z. x = Some z"
    1.33    by (cases x) (simp_all add: less_option_def)
    1.34  
    1.35 -lemma less_option_None_Some [simp]: "None < Some (x\<Colon>'a)"
    1.36 +lemma less_option_None_Some [simp]: "None < Some x"
    1.37    by (simp add: less_option_def)
    1.38  
    1.39 -lemma less_option_None_Some_code [code]: "None < Some (x\<Colon>'a) \<longleftrightarrow> True"
    1.40 +lemma less_option_None_Some_code [code]: "None < Some x \<longleftrightarrow> True"
    1.41    by simp
    1.42  
    1.43 -lemma less_option_Some [simp, code]: "Some (x\<Colon>'a) < Some y \<longleftrightarrow> x < y"
    1.44 +lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
    1.45    by (simp add: less_option_def)
    1.46  
    1.47  instance by default