summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Inductive.thy

changeset 46008 | c296c75f4cf4 |

parent 45907 | 4b41967bd77e |

child 46947 | b8c7eb0c2f89 |

1.1 --- a/src/HOL/Inductive.thy Wed Dec 28 15:08:12 2011 +0100 1.2 +++ b/src/HOL/Inductive.thy Wed Dec 28 20:03:13 2011 +0100 1.3 @@ -108,7 +108,7 @@ 1.4 and P_f: "!!S. P S ==> P(f S)" 1.5 and P_Union: "!!M. !S:M. P S ==> P(Union M)" 1.6 shows "P(lfp f)" 1.7 - using assms by (rule lfp_ordinal_induct [where P=P]) 1.8 + using assms by (rule lfp_ordinal_induct) 1.9 1.10 1.11 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 1.12 @@ -210,7 +210,7 @@ 1.13 apply (rule Un_least [THEN Un_least]) 1.14 apply (rule subset_refl, assumption) 1.15 apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) 1.16 -apply (rule monoD [where f=f], assumption) 1.17 +apply (rule monoD, assumption) 1.18 apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) 1.19 done 1.20