changeset 58249 | 180f1b3508ed |
parent 55416 | dd7992d4a61a |
child 58310 | 91ea607a34d8 |
58248:25af24e1f37b | 58249:180f1b3508ed |
---|---|
6 |
6 |
7 theory Action |
7 theory Action |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 datatype action = New | Loc nat | Free nat |
11 datatype_new action = New | Loc nat | Free nat |
12 |
12 |
13 lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y" |
13 lemma [cong]: "!!x. x = y ==> case_action a b c x = case_action a b c y" |
14 by simp |
14 by simp |
15 |
15 |
16 end |
16 end |