Thu, 04 Oct 2001 23:27:01 +0200 | wenzelm | major_prem_of: Logic.strip_assums_concl; | changeset | files |
Thu, 04 Oct 2001 16:09:12 +0200 | wenzelm | induct/cases made generic, removed simplified/stripped options; | changeset | files |
Thu, 04 Oct 2001 16:07:43 +0200 | wenzelm | improved proof by cases and induction; | changeset | files |