equal
deleted
inserted
replaced
1 (* Title: HOL/IMP/Denotation.ML |
1 (* Title: HOL/IMP/Denotation.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
3 Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
4 Copyright 1994 TUM |
4 Copyright 1994 TUM |
5 *) |
5 *) |
6 |
|
7 open Denotation; |
|
8 |
|
9 |
6 |
10 (**** mono (Gamma(b,c)) ****) |
7 (**** mono (Gamma(b,c)) ****) |
11 |
8 |
12 qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def] |
9 qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def] |
13 "mono (Gamma b c)" |
10 "mono (Gamma b c)" |