diff -r de505273c971 -r 00d4a435777f src/HOL/Bali/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Bali/ROOT.ML Mon Jan 28 17:00:19 2002 +0100 @@ -0,0 +1,13 @@ + +use_thy "WellForm"; + +(*The dynamic part of Bali, including type-safety*) +use_thy "Evaln"; +use_thy "Example"; +use_thy "TypeSafe"; +(*###use_thy "Trans";*) + +(*The Hoare logic for Bali*) +use_thy "AxExample"; +use_thy "AxSound"; +use_thy "AxCompl";