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/HOL/Algebra/abstract/Ring.thy
changeset 9390 e6b96d953965
parent 7998 3d0c34795831
child 10447 1dbd79bd3bc6 
--- a/src/HOL/Algebra/abstract/Ring.thy	Wed Jul 19 10:59:59 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy	Wed Jul 19 12:28:32 2000 +0200
@@ -24,11 +24,11 @@
 
   (* Fields *)
   inverse	:: 'a::ringS => 'a
-  "'/'/"	:: ['a, 'a] => 'a::ringS		(infixl 70)
+  "'/"		:: ['a, 'a] => 'a::ringS		(infixl 70)
 
 translations
   "a -- b" 	== "a + (-b)"
-  "a // b"	== "a * inverse b"
+  "a / b"	== "a * inverse b"
 
 (* Class ring and ring axioms *)
isabelle