replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()
(* Title: HOL/IMP/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TUM
*)
HOL_build_completed; (*Make examples fail if HOL did*)
use_thy "Examples";
use_thy "List_Examples";