equal
deleted
inserted
replaced
6 |
6 |
7 theory One |
7 theory One |
8 imports Lift |
8 imports Lift |
9 begin |
9 begin |
10 |
10 |
11 types one = "unit lift" |
11 type_synonym |
|
12 one = "unit lift" |
|
13 |
12 translations |
14 translations |
13 (type) "one" <= (type) "unit lift" |
15 (type) "one" <= (type) "unit lift" |
14 |
16 |
15 definition |
17 definition ONE :: "one" |
16 ONE :: "one" |
18 where "ONE == Def ()" |
17 where |
|
18 "ONE == Def ()" |
|
19 |
19 |
20 text {* Exhaustion and Elimination for type @{typ one} *} |
20 text {* Exhaustion and Elimination for type @{typ one} *} |
21 |
21 |
22 lemma Exh_one: "t = \<bottom> \<or> t = ONE" |
22 lemma Exh_one: "t = \<bottom> \<or> t = ONE" |
23 unfolding ONE_def by (induct t) simp_all |
23 unfolding ONE_def by (induct t) simp_all |