(* Title: HOL/Lex/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1995 TUM *) HOL_build_completed; (*Make examples fail if HOL did*) use_thy"AutoChopper"; use_thy"AutoChopper1"; use_thy"Regset_of_auto";