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.
mk_int now produces specific constants for 0 and 1.
authorberghofe
Fri, 11 Jul 2003 14:56:30 +0200
changeset 14103 afd168fdcd3a
parent 14102 8af7334af4b3
child 14104 29f726e36e5c
mk_int now produces specific constants for 0 and 1.
src/HOL/hologic.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/hologic.ML	Fri Jul 11 14:55:17 2003 +0200
+++ b/src/HOL/hologic.ML	Fri Jul 11 14:56:30 2003 +0200
@@ -321,7 +321,9 @@
 
 val intT = Type ("IntDef.int", []);
 
-fun mk_int i = number_of_const intT $ mk_bin i;
+fun mk_int 0 = Const ("0", intT)
+  | mk_int 1 = Const ("1", intT)
+  | mk_int i = number_of_const intT $ mk_bin i;
 
 
 (* real *)
isabelle