author wenzelm Sat, 18 Mar 2006 18:33:40 +0100 changeset 19287 45b8ddc2fab8 parent 19286 83404ccd270a child 19288 85b684d3fdbd
renamed const less to lt;
--- 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:
*}

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(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(blast intro: trans antisym);
apply(blast intro: refl);
done
@@ -161,12 +161,12 @@
(*
instance strord < parord
apply intro_classes;
-apply(blast intro: less_trans);
+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
--- a/doc-src/TutorialI/Types/Overloading1.thy	Sat Mar 18 09:58:49 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 @@
*}

Now @{prop"False <<= P"} is provable: