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"