src/HOL/Divides.ML
changeset 9108 9fff97d29837
parent 8935 548901d05a0e
child 9637 47d39a31eb2f
     1.1 --- a/src/HOL/Divides.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Divides.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  
     1.5  (** Less-then properties **)
     1.6  
     1.7 -val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
     1.8 -                    def_wfrec RS trans;
     1.9 +bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
    1.10 +                    def_wfrec RS trans);
    1.11  
    1.12  Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
    1.13  \                           (%f j. if j<n | n=0 then j else f (j-n))";