summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 09 Aug 2005 19:10:30 +0200 | |

changeset 17042 | da5cfaa258f7 |

parent 17041 | dee6f7047cae |

child 17043 | d3e52c3bfb07 |

moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy

src/HOL/PreList.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Wellfounded_Recursion.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/PreList.thy Tue Aug 09 15:44:24 2005 +0200 +++ b/src/HOL/PreList.thy Tue Aug 09 19:10:30 2005 +0200 @@ -14,7 +14,4 @@ Is defined separately to serve as a basis for theory ToyList in the documentation. *} -lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] - -- {* belongs to theory @{text Wellfounded_Recursion} *} - end

--- a/src/HOL/Wellfounded_Recursion.thy Tue Aug 09 15:44:24 2005 +0200 +++ b/src/HOL/Wellfounded_Recursion.thy Tue Aug 09 19:10:30 2005 +0200 @@ -56,6 +56,8 @@ |] ==> P(a)" by (unfold wf_def, blast) +lemmas wf_induct_rule = wf_induct [rule_format, case_names less, induct set: wf] + lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r" by (erule_tac a=a in wf_induct, blast)