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

6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	1	(* Title: HOLCF/IOA/ABP/Action.thy
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	2	ID: $Id$
12218 6597093b77e7 GPLed; wenzelm parents: 6008 diff changeset	3	Author: Olaf M�ller
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	4	*)
d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	5
17244 0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	6	header {* The set of all actions of the system *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	7
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	8	theory Action
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	9	imports Main
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	10	begin
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	11
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	12	datatype action = New \| Loc nat \| Free nat
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	13
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	14	lemma [cong]: "!!x. x = y ==> action_case a b c x = action_case a b c y"
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	15	by simp
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	16
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	17	ML {* use_legacy_bindings (the_context ()) *}
0b2ff9541727 converted to Isar theory format; wenzelm parents: 14981 diff changeset	18
6008 d0e9b1619468 Memory storage case study from PhD p.240; mueller parents: diff changeset	19	end

author	paulson
	Wed, 14 Dec 2005 16:13:09 +0100
changeset 18404	aa27c10a040e
parent 17244	0b2ff9541727
child 19740	6b38551d0798
permissions	-rw-r--r--