Theorems for converting between wf and wfP are now declared
authorberghofe
Wed Feb 07 17:30:53 2007 +0100 (2007-02-07)
changeset 222646a65e9b2ae05
parent 22263 990a638e6f69
child 22265 3c5c6bdf61de
Theorems for converting between wf and wfP are now declared
as hints.
src/HOL/Recdef.thy
     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 . . . *)