author | berghofe |

Wed Feb 07 17:30:53 2007 +0100 (2007-02-07) | |

changeset 22264 | 6a65e9b2ae05 |

parent 22263 | 990a638e6f69 |

child 22265 | 3c5c6bdf61de |

Theorems for converting between wf and wfP are now declared

as hints.

as hints.

1.1 --- a/src/HOL/Recdef.thy Wed Feb 07 17:29:41 2007 +0100 1.2 +++ b/src/HOL/Recdef.thy Wed Feb 07 17:30:53 2007 +0100 1.3 @@ -79,6 +79,8 @@ 1.4 wf_pred_nat 1.5 wf_same_fst 1.6 wf_empty 1.7 + wf_implies_wfP 1.8 + wfP_implies_wf 1.9 1.10 (* The following should really go into Datatype or Finite_Set, but 1.11 each one lacks the other theory as a parent . . . *)