# HG changeset patch
# User paulson
# Date 932391342 -7200
# Node ID e01513f1390a8bc549cfb429d1704d638ecd16c5
# Parent  77d596a5ffae66f6074cd85d07664dad548556c1
NatBin: binary arithmetic for the naturals

diff -r 77d596a5ffae -r e01513f1390a src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jul 19 15:32:14 1999 +0200
+++ b/src/HOL/Main.thy	Mon Jul 19 15:35:42 1999 +0200
@@ -1,4 +1,4 @@
 
 (*theory Main includes everything*)
 
-Main = IntDiv + Map + Recdef + Record + RelPow + Sexp + String + Calculation
+Main = NatBin + Map + Recdef + Record + RelPow + Sexp + String + Calculation