isabelle: src/HOL/IMP/Com.thy@720b72513ae5 (annotated)

58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 58310 diff changeset	1	section "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
58310 91ea607a34d8 updated news blanchet parents: 58305 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
	Sun, 05 Jul 2020 11:06:09 +0200
changeset 71999	720b72513ae5
parent 58889	5b7a9633cfa8
child 80914	d97fdabd9e2b
permissions	-rw-r--r--