Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/Types/Overloading1.thy
changeset 19287 45b8ddc2fab8
parent 17914 99ead7a7eb42 
--- 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:
isabelle