# 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