src/HOL/Wfrec.thy
 changeset 61799 4cf66f21b764 parent 60758 d8d85a8172b5 child 63040 eb4ddd18d635
```     1.1 --- a/src/HOL/Wfrec.thy	Mon Dec 07 10:23:50 2015 +0100
1.2 +++ b/src/HOL/Wfrec.thy	Mon Dec 07 10:38:04 2015 +0100
1.3 @@ -79,11 +79,11 @@
1.4    finally show "wfrec R F x = F (wfrec R F) x" .
1.5  qed
1.6
1.7 -subsection \<open>Wellfoundedness of @{text same_fst}\<close>
1.8 +subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
1.9
1.10  definition same_fst :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> ('b \<times> 'b) set) \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set" where
1.11    "same_fst P R = {((x', y'), (x, y)) . x' = x \<and> P x \<and> (y',y) \<in> R x}"
1.12 -   --\<open>For @{const wfrec} declarations where the first n parameters
1.13 +   \<comment>\<open>For @{const wfrec} declarations where the first n parameters
1.14         stay unchanged in the recursive call.\<close>
1.15
1.16  lemma same_fstI [intro!]: "P x \<Longrightarrow> (y', y) \<in> R x \<Longrightarrow> ((x, y'), (x, y)) \<in> same_fst P R"
```