equal
deleted
inserted
replaced
6 and of extended type definition theorems |
6 and of extended type definition theorems |
7 *) |
7 *) |
8 |
8 |
9 header {* Type Definition Theorems *} |
9 header {* Type Definition Theorems *} |
10 |
10 |
11 theory TdThs imports Main begin |
11 theory TdThs |
|
12 imports Main |
|
13 begin |
12 |
14 |
13 section "More lemmas about normal type definitions" |
15 section "More lemmas about normal type definitions" |
14 |
16 |
15 lemma |
17 lemma |
16 tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and |
18 tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A" and |