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/Library/EfficientNat.thy
changeset 18757 f0d901bc0686
parent 18708 4b3dadb4fe33
child 18851 9502ce541f01 
--- a/src/HOL/Library/EfficientNat.thy	Mon Jan 23 14:06:40 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Mon Jan 23 14:07:52 2006 +0100
@@ -52,12 +52,12 @@
   int ("(_)")
 
 (* code_syntax_tyco nat
-  ml (atom "InfInt.int")
-  haskell (atom "Integer")
+  ml (target_atom "InfInt.int")
+  haskell (target_atom "Integer")
 
 code_syntax_const 0 :: nat
   ml ("0 : InfInt.int")
-  haskell (atom "0")
+  haskell (target_atom "0")
 
 code_syntax_const Suc
   ml (infixl 8 "_ + 1")
isabelle