dropped square syntax
authorhaftmann
Fri Oct 26 21:22:18 2007 +0200 (2007-10-26)
changeset 25207d58c14280367
parent 25206 9c84ec7217a9
child 25208 1a7318a04068
dropped square syntax
src/HOL/Orderings.thy
src/HOL/Wellfounded_Recursion.thy
     1.1 --- a/src/HOL/Orderings.thy	Fri Oct 26 21:22:17 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Oct 26 21:22:18 2007 +0200
     1.3 @@ -20,11 +20,6 @@
     1.4    assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
     1.5  begin
     1.6  
     1.7 -notation (input)
     1.8 -  less_eq (infix "\<sqsubseteq>" 50)
     1.9 -and
    1.10 -  less    (infix "\<sqsubset>" 50)
    1.11 -
    1.12  text {* Reflexivity. *}
    1.13  
    1.14  lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
    1.15 @@ -124,7 +119,7 @@
    1.16  subsection {* Linear (total) orders *}
    1.17  
    1.18  class linorder = order +
    1.19 -  assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
    1.20 +  assumes linear: "x \<le> y \<or> y \<le> x"
    1.21  begin
    1.22  
    1.23  lemma less_linear: "x < y \<or> x = y \<or> y < x"
     2.1 --- a/src/HOL/Wellfounded_Recursion.thy	Fri Oct 26 21:22:17 2007 +0200
     2.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Fri Oct 26 21:22:18 2007 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4    "acyclicP r == acyclic {(x, y). r x y}"
     2.5  
     2.6  class wellorder = linorder +
     2.7 -  assumes wf: "wf {(x, y). x \<sqsubset> y}"
     2.8 +  assumes wf: "wf {(x, y). x < y}"
     2.9  
    2.10  
    2.11  lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"