| changeset 67613 | ce654b0e6d69 |
| parent 62002 | f1599e98c4d0 |
| 67610:4939494ed791 | 67613:ce654b0e6d69 |
|---|---|
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 datatype action = New | Loc nat | Free nat |
11 datatype 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]: "\<And>x. x = y \<Longrightarrow> case_action a b c x = case_action a b c y" |
14 by simp |
14 by simp |
15 |
15 |
16 end |
16 end |