isabelle: src/HOL/IMP/Com.thy@600781e03bf6 (annotated)

43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	1	header "IMP --- A Simple Imperative Language"
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	2
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	3	theory Com imports BExp begin
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	4
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	5	datatype
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	6	com = SKIP
45321 b227989b6ee6 more IMP text fragments kleing parents: 45212 diff changeset	7	\| Assign vname aexp ("_ ::= _" [1000, 61] 61)
52046 bc01725d7918 replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time nipkow parents: 47818 diff changeset	8	\| Seq com com ("_;;/ _" [60, 61] 60)
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	9	\| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	10	\| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	11
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	12	end

author	wenzelm
	Wed, 12 Mar 2014 17:02:05 +0100
changeset 56065	600781e03bf6
parent 52046	bc01725d7918
child 58305	57752a91eec4
permissions	-rw-r--r--