src/HOL/Bali/ROOT.ML
author schirmer
Mon, 28 Jan 2002 17:00:19 +0100
changeset 12854 00d4a435777f
child 12859 f63315dfffd4
permissions -rw-r--r--
Isabelle/Bali sources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     1
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
use_thy "WellForm";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
(*The dynamic part of Bali, including type-safety*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
use_thy "Evaln";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
use_thy "Example"; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
use_thy "TypeSafe";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
(*###use_thy "Trans";*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
(*The Hoare logic for Bali*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
use_thy "AxExample";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
use_thy "AxSound";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
use_thy "AxCompl";