# HG changeset patch
# User wenzelm
# Date 880559022 -3600
# Node ID 7fe9723d579bb4d6a38e6f8349bdbfb9e1178d3f
# Parent  66da34945f8b84bd03a6e3f2658874d1cb677303
added dest_nat;

diff -r 66da34945f8b -r 7fe9723d579b src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Nov 26 16:42:56 1997 +0100
+++ b/src/HOL/hologic.ML	Wed Nov 26 16:43:42 1997 +0100
@@ -36,6 +36,7 @@
   val mk_Suc: term -> term
   val dest_Suc: term -> term
   val mk_nat: int -> term
+  val dest_nat: term -> int
 end;
 
 
@@ -112,16 +113,25 @@
 
 val natT = Type ("nat", []);
 
+
 val zero = Const ("0", natT);
-fun is_zero t = t = zero;
+
+fun is_zero (Const ("0", _)) = true
+  | is_zero _ = false;
+
 
 fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
 
 fun dest_Suc (Const ("Suc", _) $ t) = t
   | dest_Suc t = raise TERM ("dest_Suc", [t]);
 
+
 fun mk_nat 0 = zero
   | mk_nat n = mk_Suc (mk_nat (n - 1));
 
+fun dest_nat (Const ("0", _)) = 0
+  | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
+  | dest_nat t = raise TERM ("dest_nat", [t]);
+
 
 end;