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

src/ZF/WF.ML

changeset 485 | 5e00a676a211 |

parent 443 | 10884e64c241 |

child 494 | 3686157a5a51 |

--- a/src/ZF/WF.ML Tue Jul 26 13:21:20 1994 +0200 +++ b/src/ZF/WF.ML Tue Jul 26 13:44:42 1994 +0200 @@ -95,7 +95,7 @@ rename_last_tac a ["1"] (i+1), ares_tac prems i]; -(*The form of this rule is designed to match wfI2*) +(*The form of this rule is designed to match wfI*) val wfr::amem::prems = goal WF.thy "[| wf(r); a:A; field(r)<=A; \ \ !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x) \ @@ -133,7 +133,7 @@ \ ==> wf(r)"; by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1); by (REPEAT (ares_tac [indhyp] 1)); -val wfI2 = result(); +val wfI = result(); (*** Properties of well-founded relations ***)