equal
deleted
inserted
replaced
426 thus ?case by simp |
426 thus ?case by simp |
427 qed |
427 qed |
428 qed |
428 qed |
429 |
429 |
430 realizers |
430 realizers |
431 NatDef.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n" |
431 Nat.nat_induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n" |
432 "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h" |
432 "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h" |
433 |
433 |
434 NatDef.nat_induct: "Null" |
434 Nat.nat_induct: "Null" |
435 "\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _" |
435 "\<Lambda>P n. nat_induct \<cdot> _ \<cdot> _" |
436 |
436 |
437 Nat.nat.induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n" |
437 Nat.nat.induct (P): "\<lambda>P n p0 ps. nat_rec p0 ps n" |
438 "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h" |
438 "\<Lambda>P n p0 (h: _) ps. nat_ind_realizer \<cdot> _ \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h" |
439 |
439 |