# HG changeset patch
# User wenzelm
# Date 849109557 -3600
# Node ID 8ad8ee759d9fba34967a914e05f366d833cb4c12
# Parent  c8154379738c136269d3d042f64aa45ddfb29529
moved "1", "2" to syntax section;

diff -r c8154379738c -r 8ad8ee759d9f src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Nov 27 16:42:48 1996 +0100
+++ b/src/HOL/Nat.thy	Wed Nov 27 16:45:57 1996 +0100
@@ -44,8 +44,6 @@
 
 consts
   "0"       :: nat                ("0")
-  "1"       :: nat                ("1")
-  "2"       :: nat                ("2")
   Suc       :: nat => nat
   nat_case  :: ['a, nat => 'a, nat] => 'a
   pred_nat  :: "(nat * nat) set"
@@ -53,6 +51,10 @@
 
   Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
 
+syntax
+  "1"       :: nat                ("1")
+  "2"       :: nat                ("2")
+
 translations
    "1"  == "Suc(0)"
    "2"  == "Suc(1)"