isabelle: src/HOL/ROOT.ML@df8448bc7a8b (annotated)

1264 3eb91524b938 added local simpsets; removed IOA from 'make test' clasohm parents: 1165 diff changeset	1	(* Title: HOL/ROOT.ML
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
23166 45f3c90b2d27 proper loading of ML files (in HOL.thy); wenzelm parents: 22997 diff changeset	3
7739 bfe45b716dfc tuned comment; wenzelm parents: 7703 diff changeset	4	Classical Higher-order Logic.
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	6
23166 45f3c90b2d27 proper loading of ML files (in HOL.thy); wenzelm parents: 22997 diff changeset	7	use_thy "Main";
10275 558f7569026e tuned; wenzelm parents: 10263 diff changeset	8
10263 9cc180732945 path_add "~~/src/HOL/Library"; wenzelm parents: 9891 diff changeset	9	path_add "~~/src/HOL/Library";