Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added constant abs.
authornipkow
Fri, 05 May 2000 18:24:06 +0200
changeset 8800 e3688ef49f12
parent 8799 89e9deef4bcb
child 8801 9d01c9a26134
Added constant abs.
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Fri May 05 17:49:54 2000 +0200
+++ b/src/HOL/HOL.thy	Fri May 05 18:24:06 2000 +0200
@@ -62,6 +62,7 @@
   "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
   -             :: "['a::minus, 'a] => 'a"          (infixl 65)
   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
+  abs		:: "('a::minus) => 'a"
   *             :: "['a::times, 'a] => 'a"          (infixl 70)
   (*See Nat.thy for "^"*)
isabelle