isabelle: src/HOL/IMP/Com.thy@f961c1fdff50 (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
9241 f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 8029 diff changeset	19	arities loc :: 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
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	oheimb
	Tue, 04 Jul 2000 10:54:46 +0200
changeset 9241	f961c1fdff50
parent 8029	05446a898852
child 12338	de0f4a63baa5
permissions	-rw-r--r--