src/FOL/ex/Nat2.thy
changeset 1322 9b3d3362a048
parent 352 fd3ab8bcb69d
child 1473 e8d4606e6502
--- a/src/FOL/ex/Nat2.thy	Tue Nov 07 12:57:20 1995 +0100
+++ b/src/FOL/ex/Nat2.thy	Tue Nov 07 12:58:17 1995 +0100
@@ -12,10 +12,10 @@
 arities nat :: term
 
 consts
- succ,pred :: "nat => nat"
-       "0" :: "nat"	("0")
-       "+" :: "[nat,nat] => nat" (infixr 90)
-  "<","<=" :: "[nat,nat] => o"   (infixr 70)
+ succ,pred :: nat => nat  
+       "0" :: nat  	("0")
+       "+" :: [nat,nat] => nat   (infixr 90)
+  "<","<=" :: [nat,nat] => o     (infixr 70)
 
 rules
  pred_0		"pred(0) = 0"