| changeset 5761 | a396eff81fda |
| parent 5715 | 5fc697ad232b |
| child 5788 | e3a98a7c0634 |
--- a/src/HOL/Prod.ML Fri Oct 23 22:36:15 1998 +0200 +++ b/src/HOL/Prod.ML Fri Oct 23 22:36:49 1998 +0200 @@ -432,6 +432,11 @@ Addsimprocs [unit_eq_proc]; +Goal "P () ==> P x"; +by (Simp_tac 1); +qed "unit_induct"; + + (*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u), replacing it by f rather than by %u.f(). *) Goal "(%u::unit. f()) = f";