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.
src/ZF/ex/Integ.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab 
--- a/src/ZF/ex/Integ.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Integ.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,17 +8,17 @@
 
 Integ = EquivClass + Arith +
 consts
-    intrel,integ::      "i"
-    znat	::	"i=>i"		("$# _" [80] 80)
-    zminus	::	"i=>i"		("$~ _" [80] 80)
-    znegative	::	"i=>o"
-    zmagnitude	::	"i=>i"
-    "$*"        ::      "[i,i]=>i"      (infixl 70)
-    "$'/"       ::      "[i,i]=>i"      (infixl 70) 
-    "$'/'/"     ::      "[i,i]=>i"      (infixl 70)
-    "$+"	::      "[i,i]=>i"      (infixl 65)
-    "$-"        ::      "[i,i]=>i"      (infixl 65)
-    "$<"	:: 	"[i,i]=>o"  	(infixl 50)
+    intrel,integ::      i
+    znat	::	i=>i		("$# _" [80] 80)
+    zminus	::	i=>i		("$~ _" [80] 80)
+    znegative	::	i=>o
+    zmagnitude	::	i=>i
+    "$*"        ::      [i,i]=>i      (infixl 70)
+    "$'/"       ::      [i,i]=>i      (infixl 70) 
+    "$'/'/"     ::      [i,i]=>i      (infixl 70)
+    "$+"	::      [i,i]=>i      (infixl 65)
+    "$-"        ::      [i,i]=>i      (infixl 65)
+    "$<"	:: 	[i,i]=>o  	(infixl 50)
 
 defs
isabelle