| changeset 41589 | bbd861837ebc |
| parent 27362 | a6dc1769fdda |
| child 42174 | d0be2722ce9f |
| 41588:9546828c0eb3 | 41589:bbd861837ebc |
|---|---|
1 (* Title: HOL/IMPP/Com.thy |
1 (* Title: HOL/IMPP/Com.thy |
2 ID: $Id$ |
|
3 Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM |
2 Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM |
4 Copyright 1999 TUM |
|
5 *) |
3 *) |
6 |
4 |
7 header {* Semantics of arithmetic and boolean expressions, Syntax of commands *} |
5 header {* Semantics of arithmetic and boolean expressions, Syntax of commands *} |
8 |
6 |
9 theory Com |
7 theory Com |