# HG changeset patch # User wenzelm # Date 1002187710 -7200 # Node ID 8a86409108fe38ead60afe5615dd477aff070fd3 # Parent 744399c9dd6a76ead2168e803701ce0b395cfa20 * moved induct/cases attributes to Pure, added 'print_induct_rules' command; diff -r 744399c9dd6a -r 8a86409108fe NEWS --- a/NEWS Thu Oct 04 11:28:12 2001 +0200 +++ b/NEWS Thu Oct 04 11:28:30 2001 +0200 @@ -24,6 +24,9 @@ * Isar/HOL: 'inductive' now longer features separate (collective) attributes for 'intros'; +* moved induct/cases attributes to Pure, added 'print_induct_rules' +command; + *** HOL ***