isabelle: src/HOL/HOLCF/IOA/Storage/Action.thy@dd7992d4a61a (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40945 diff changeset	1	(* Title: HOL/HOLCF/IOA/Storage/Action.thy
40945 b8703f63bfb2 recoded latin1 as utf8; wenzelm parents: 40774 diff changeset	2	Author: Olaf Müller
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	3	*)
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	4
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	5	header {* The set of all actions of the system *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7	theory Action
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	imports Main
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10
55416 dd7992d4a61a adapted theories to 'xxx_case' to 'case_xxx' blanchet parents: 42151 diff changeset	11	datatype action = New \| Loc nat \| Free nat
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12
55416 dd7992d4a61a adapted theories to 'xxx_case' to 'case_xxx' blanchet parents: 42151 diff changeset	13	lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y"
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	by simp
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	15
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	16	end

author	blanchet
	Wed, 12 Feb 2014 08:35:57 +0100
changeset 55416	dd7992d4a61a
parent 42151	4da4fc77664b
child 58249	180f1b3508ed
permissions	-rw-r--r--