# HG changeset patch
# User wenzelm
# Date 1142703220 -3600
# Node ID 45b8ddc2fab83437df960c8b12613aa9cbc5ddb8
# Parent  83404ccd270a8c511753d7797fa0405ef2593294
renamed const less to lt;

diff -r 83404ccd270a -r 45b8ddc2fab8 doc-src/TutorialI/Types/Axioms.thy
--- a/doc-src/TutorialI/Types/Axioms.thy	Sat Mar 18 09:58:49 2006 +0100
+++ b/doc-src/TutorialI/Types/Axioms.thy	Sat Mar 18 18:33:40 2006 +0100
@@ -20,7 +20,7 @@
 refl:    "x <<= x"
 trans:   "\<lbrakk> x <<= y; y <<= z \<rbrakk> \<Longrightarrow> x <<= z"
 antisym: "\<lbrakk> x <<= y; y <<= x \<rbrakk> \<Longrightarrow> x = y"
-less_le: "x << y = (x <<= y \<and> x \<noteq> y)"
+lt_le:   "x << y = (x <<= y \<and> x \<noteq> y)"
 
 text{*\noindent
 The first three axioms are the familiar ones, and the final one
@@ -29,7 +29,7 @@
 @{text parord}. For example, the axiom @{thm[source]refl} really is
 @{thm[show_sorts]refl}.
 
-We have not made @{thm[source]less_le} a global definition because it would
+We have not made @{thm[source] lt_le} a global definition because it would
 fix once and for all that @{text"<<"} is defined in terms of @{text"<<="} and
 never the other way around. Below you will see why we want to avoid this
 asymmetry. The drawback of our choice is that
@@ -54,7 +54,7 @@
 when the proposition is not a theorem.  The proof is easy:
 *}
 
-by(simp add: less_le antisym);
+by(simp add: lt_le antisym);
 
 text{* We could now continue in this vein and develop a whole theory of
 results about partial orders. Eventually we will want to apply these results
@@ -74,7 +74,7 @@
 of @{text"<<"} and @{text"<<="} at type @{typ bool}:
 *}
 
-apply(simp_all (no_asm_use) only: le_bool_def less_bool_def);
+apply(simp_all (no_asm_use) only: le_bool_def lt_bool_def);
 by(blast, blast, blast, blast);
 
 text{*\noindent
@@ -108,7 +108,7 @@
 *}
 
 lemma "\<And>x::'a::linord. x << y \<or> x = y \<or> y << x";
-apply(simp add: less_le);
+apply(simp add: lt_le);
 apply(insert linear);
 apply blast;
 done
@@ -130,7 +130,7 @@
 
 axclass strord < ordrel
 irrefl:     "\<not> x << x"
-less_trans: "\<lbrakk> x << y; y << z \<rbrakk> \<Longrightarrow> x << z"
+lt_trans:   "\<lbrakk> x << y; y << z \<rbrakk> \<Longrightarrow> x << z"
 le_less:    "x <<= y = (x << y \<or> x = y)"
 
 text{*\noindent
@@ -147,7 +147,7 @@
 are easily proved:
 *}
 
-  apply(simp_all (no_asm_use) add: less_le);
+  apply(simp_all (no_asm_use) add: lt_le);
  apply(blast intro: trans antisym);
 apply(blast intro: refl);
 done
@@ -161,12 +161,12 @@
 (*
 instance strord < parord
 apply intro_classes;
-apply(simp_all (no_asm_use) add: le_less);
-apply(blast intro: less_trans);
+apply(simp_all (no_asm_use) add: le_lt);
+apply(blast intro: lt_trans);
 apply(erule disjE);
 apply(erule disjE);
 apply(rule irrefl[THEN notE]);
-apply(rule less_trans, assumption, assumption);
+apply(rule lt_trans, assumption, assumption);
 apply blast;apply blast;
 apply(blast intro: irrefl[THEN notE]);
 done
diff -r 83404ccd270a -r 45b8ddc2fab8 doc-src/TutorialI/Types/Overloading1.thy
--- a/doc-src/TutorialI/Types/Overloading1.thy	Sat Mar 18 09:58:49 2006 +0100
+++ b/doc-src/TutorialI/Types/Overloading1.thy	Sat Mar 18 18:33:40 2006 +0100
@@ -21,8 +21,8 @@
 instances:
 *}
 
-consts less :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<"  50)
-       le   :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<=" 50)
+consts lt :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<"  50)
+       le :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool"     (infixl "<<=" 50)
 
 text{*\noindent
 Note that only one occurrence of a type variable in a type needs to be
@@ -54,8 +54,8 @@
 *}
 
 defs (overloaded)
-le_bool_def:  "P <<= Q \<equiv> P \<longrightarrow> Q"
-less_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
+le_bool_def: "P <<= Q \<equiv> P \<longrightarrow> Q"
+lt_bool_def: "P << Q \<equiv> \<not>P \<and> Q"
 
 text{*\noindent
 Now @{prop"False <<= P"} is provable: