| changeset 41589 | bbd861837ebc |
| parent 27362 | a6dc1769fdda |
| child 42174 | d0be2722ce9f |
| 41588:9546828c0eb3 | 41589:bbd861837ebc |
|---|---|
1 (* Title: HOL/IMP/Com.thy |
1 (* Title: HOL/IMP/Com.thy |
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
2 Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
4 Isar Version: Gerwin Klein, 2001 |
3 Author: Gerwin Klein |
5 Copyright 1994 TUM |
|
6 *) |
4 *) |
7 |
5 |
8 header "Syntax of Commands" |
6 header "Syntax of Commands" |
9 |
7 |
10 theory Com imports Main begin |
8 theory Com imports Main begin |