1
(* Title: HOL/IMP/ROOT.ML
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1995 TUM
5
*)
6
7
HOL_build_completed; (*Make examples fail if HOL did*)
8
9
use_thy "Examples";
10
use_thy "List_Examples";