isabelle: src/HOL/IMP/Com.thy@de0f4a63baa5 (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
9241 f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 8029 diff changeset	12	types
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1481 diff changeset	13	loc
9241 f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 8029 diff changeset	14	val = nat (* or anything else, nat used in examples *)
f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 8029 diff changeset	15	state = loc => val
f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 8029 diff changeset	16	aexp = state => val
1696 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
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 9241 diff changeset	19	arities loc :: type
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
9241 f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 8029 diff changeset	23	\| ":==" loc aexp (infixl 60)
1481 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	wenzelm
	Sat, 01 Dec 2001 18:52:32 +0100
changeset 12338	de0f4a63baa5
parent 9241	f961c1fdff50
child 12431	07ec657249e5
permissions	-rw-r--r--