src/HOL/ex/Factorization.ML
Tue, 28 Mar 2000 17:31:36 +0200 mods because of weak_case_cong
Mon, 20 Mar 2000 18:24:11 +0100 the perm_rules variable is no longer needed
Mon, 13 Mar 2000 16:23:34 +0100 case_tac now subsumes both boolean and datatype cases;
Mon, 13 Mar 2000 12:51:10 +0100 exhaust_tac -> cases_tac
Wed, 08 Mar 2000 16:14:12 +0100 new theory ex/Factorization