src/HOL/Recdef.thy
changeset 10653 55f33da63366
parent 10212 33fe2d701ddd
child 10773 0deff0197496
     1.1 --- a/src/HOL/Recdef.thy	Wed Dec 13 09:30:59 2000 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Wed Dec 13 09:32:55 2000 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4    wf_inv_image
     1.5    wf_measure
     1.6    wf_pred_nat
     1.7 +  wf_same_fst
     1.8    wf_empty
     1.9  
    1.10  end