# HG changeset patch
# User haftmann
# Date 1193426538 -7200
# Node ID d58c14280367feb9a7fe42a08dc767e1739185cc
# Parent  9c84ec7217a9d0b44305eccde0ad4e320103b5a6
dropped square syntax

diff -r 9c84ec7217a9 -r d58c14280367 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Oct 26 21:22:17 2007 +0200
+++ b/src/HOL/Orderings.thy	Fri Oct 26 21:22:18 2007 +0200
@@ -20,11 +20,6 @@
   assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
 begin
 
-notation (input)
-  less_eq (infix "\<sqsubseteq>" 50)
-and
-  less    (infix "\<sqsubset>" 50)
-
 text {* Reflexivity. *}
 
 lemma eq_refl: "x = y \<Longrightarrow> x \<le> y"
@@ -124,7 +119,7 @@
 subsection {* Linear (total) orders *}
 
 class linorder = order +
-  assumes linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+  assumes linear: "x \<le> y \<or> y \<le> x"
 begin
 
 lemma less_linear: "x < y \<or> x = y \<or> y < x"
diff -r 9c84ec7217a9 -r d58c14280367 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Fri Oct 26 21:22:17 2007 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Fri Oct 26 21:22:18 2007 +0200
@@ -41,7 +41,7 @@
   "acyclicP r == acyclic {(x, y). r x y}"
 
 class wellorder = linorder +
-  assumes wf: "wf {(x, y). x \<sqsubset> y}"
+  assumes wf: "wf {(x, y). x < y}"
 
 
 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"