equal
deleted
inserted
replaced
12 text {* |
12 text {* |
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 letter = A | B |
18 |
18 |
19 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool" |
19 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool" |
20 where |
20 where |
21 emb0 [Pure.intro]: "emb [] bs" |
21 emb0 [Pure.intro]: "emb [] bs" |
22 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)" |
22 | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)" |