equal
deleted
inserted
replaced
77 |
77 |
78 lemma wf_id: "wf r \<Longrightarrow> wf(id r)" |
78 lemma wf_id: "wf r \<Longrightarrow> wf(id r)" |
79 by simp; |
79 by simp; |
80 |
80 |
81 text{*\noindent |
81 text{*\noindent |
82 and should have appended the following hint to our above definition: |
82 and should have appended the following hint to our definition above: |
83 \indexbold{*recdef_wf} |
83 \indexbold{*recdef_wf} |
84 *} |
84 *} |
85 (*<*) |
85 (*<*) |
86 consts g :: "nat \<Rightarrow> nat" |
86 consts g :: "nat \<Rightarrow> nat" |
87 recdef g "id(less_than)" |
87 recdef g "id(less_than)" |