isabelle: src/HOL/IMP/Com.thy@05446a898852 (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	1	(* Title: HOL/IMP/Com.thy
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	2	ID: $Id$
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	3	Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	4	Copyright 1994 TUM
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	5
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	6	Semantics of arithmetic and boolean expressions
e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	7	Syntax of commands
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	8	*)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	9
8029 05446a898852 Basis now Main. nipkow parents: 5183 diff changeset	10	Com = Main +
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	11
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	12	types
e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	13	val
e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	14	loc
e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	15	state = "loc => val"
e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	16	aexp = "state => val"
e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	17	bexp = state => bool
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	18
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	19	arities loc,val :: term
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	20
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	21	datatype
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	22	com = SKIP
1481 03f096efa26d Modified datatype com. nipkow parents: 1476 diff changeset	23	\| ":=" loc aexp (infixl 60)
03f096efa26d Modified datatype com. nipkow parents: 1476 diff changeset	24	\| Semi com com ("_; _" [60, 60] 10)
03f096efa26d Modified datatype com. nipkow parents: 1476 diff changeset	25	\| Cond bexp com com ("IF _ THEN _ ELSE _" 60)
03f096efa26d Modified datatype com. nipkow parents: 1476 diff changeset	26	\| While bexp com ("WHILE _ DO _" 60)
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	27
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	28	end

author	nipkow
	Wed, 24 Nov 1999 12:12:36 +0100
changeset 8029	05446a898852
parent 5183	89f162de39cf
child 9241	f961c1fdff50
permissions	-rw-r--r--