src/HOL/Extraction.thy
changeset 13452 278f2cba42ab
parent 13403 bc2b32ee62fd
child 13468 71118807d303
     1.1 --- a/src/HOL/Extraction.thy	Mon Aug 05 14:28:31 2002 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Mon Aug 05 14:29:20 2002 +0200
     1.3 @@ -428,10 +428,10 @@
     1.4  qed
     1.5  
     1.6  realizers
     1.7 -  NatDef.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"
     1.8 +  Nat.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"
     1.9      "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
    1.10  
    1.11 -  NatDef.nat_induct: "Null"
    1.12 +  Nat.nat_induct: "Null"
    1.13      "\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _"
    1.14  
    1.15    Nat.nat.induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n"