isabelle: src/HOL/Hoare/ROOT.ML@5d7a7e439cec (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1363 diff changeset	1	(* Title: HOL/IMP/ROOT.ML
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1363 diff changeset	3	Author: Tobias Nipkow
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	4	Copyright 1995 TUM
5e1c0540f285 New directory. nipkow parents: diff changeset	5	*)
5e1c0540f285 New directory. nipkow parents: diff changeset	6
1465 5d7a7e439cec expanded tabs clasohm parents: 1363 diff changeset	7	HOL_build_completed; (Make examples fail if HOL did)
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	8
5e1c0540f285 New directory. nipkow parents: diff changeset	9	use_thy "Examples";
1363 7bdc4699ef4d Added List_Examples nipkow parents: 1351 diff changeset	10	use_thy "List_Examples";