src/HOL/Hoare/ROOT.ML
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14028 ff6eb32b30a1
child 24104 719fbe4fb77f
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/IMP/ROOT.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1998-2003 TUM
     5 *)
     6 
     7 time_use_thy "Examples";
     8 time_use_thy "ExamplesAbort";
     9 time_use_thy "Pointers0";
    10 time_use_thy "Pointer_Examples";
    11 time_use_thy "Pointer_ExamplesAbort";
    12 time_use_thy "SchorrWaite";
    13 time_use_thy "Separation";