src/HOL/Integ/ROOT.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2280 eb2ba30c2981
child 5078 7b5ea59c0275
permissions -rw-r--r--
added AxClasses test;
clasohm@1465
     1
(*  Title:      HOL/Integ/ROOT
clasohm@925
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@925
     4
    Copyright   1995  University of Cambridge
clasohm@925
     5
clasohm@1165
     6
The Integers in HOL (ported from ZF by Riccardo Mattolini)
clasohm@925
     7
*)
clasohm@925
     8
clasohm@1165
     9
HOL_build_completed;    (*Cause examples to fail if HOL did*)
clasohm@925
    10
paulson@1632
    11
time_use_thy "Bin";
nipkow@2280
    12
time_use_thy "IntRing";