equal
deleted
inserted
replaced
13 Formalization by Stefan Berghofer and Monika Seisenberger, |
13 Formalization by Stefan Berghofer and Monika Seisenberger, |
14 based on Coquand and Fridlender \cite{Coquand93}. |
14 based on Coquand and Fridlender \cite{Coquand93}. |
15 *} |
15 *} |
16 |
16 |
17 datatype_new letter = A | B |
17 datatype_new letter = A | B |
18 |
|
19 datatype_compat letter |
|
20 |
18 |
21 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool" |
19 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool" |
22 where |
20 where |
23 emb0 [Pure.intro]: "emb [] bs" |
21 emb0 [Pure.intro]: "emb [] bs" |
24 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)" |
22 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)" |