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.
"arbitrary" merely abbreviates undefined
authorhaftmann
Fri, 24 Oct 2008 17:48:34 +0200
changeset 28682 5de9fc98ad96
parent 28681 e8664643f543
child 28683 59c01ec6cb8d
"arbitrary" merely abbreviates undefined
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Fri Oct 24 17:48:33 2008 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 24 17:48:34 2008 +0200
@@ -202,11 +202,8 @@
 axiomatization
   undefined :: 'a
 
-consts
-  arbitrary :: 'a
-
-finalconsts
-  arbitrary
+abbreviation (input)
+  "arbitrary \<equiv> undefined"
 
 
 subsubsection {* Generic classes and algebraic operations *}
isabelle