481
|
1 |
(* Title: ZF/IMP/ROOT.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM
|
|
4 |
Copyright 1994 TUM
|
|
5 |
|
|
6 |
Executes the formalization of the denotational and operational semantics of a
|
|
7 |
simple while-language, including an equivalence proof. The whole development
|
|
8 |
essentially formalizes/transcribes chapters 2 and 5 of
|
|
9 |
|
|
10 |
Glynn Winskel. The Formal Semantics of Programming Languages.
|
|
11 |
MIT Press, 1993.
|
|
12 |
|
|
13 |
*)
|
|
14 |
|
|
15 |
ZF_build_completed; (*Make examples fail if ZF did*)
|
|
16 |
|
|
17 |
writeln"Root file for ZF/IMP";
|
|
18 |
proof_timing := true;
|
|
19 |
loadpath := [".","IMP"];
|
910
|
20 |
time_use_thy "Equiv" handle _ => exit 1;
|