summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Inductive.thy

changeset 32587 | caa5ada96a00 |

parent 31949 | 3f933687fae9 |

child 32652 | 3175e23b79f3 |

child 32683 | 7c1fe854ca6a |

--- a/src/HOL/Inductive.thy Wed Sep 16 09:04:41 2009 +0200 +++ b/src/HOL/Inductive.thy Wed Sep 16 13:43:05 2009 +0200 @@ -111,8 +111,7 @@ and P_f: "!!S. P S ==> P(f S)" and P_Union: "!!M. !S:M. P S ==> P(Union M)" shows "P(lfp f)" - using assms unfolding Sup_set_eq [symmetric] - by (rule lfp_ordinal_induct [where P=P]) + using assms by (rule lfp_ordinal_induct [where P=P]) text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},