src/HOL/Option.ML
Mon, 03 Nov 1997 09:57:35 +0100 nipkow expand_option_case -> split_option_case
Thu, 30 Oct 1997 09:45:03 +0100 nipkow For each datatype `t' there is now a theorem `split_t_case' of the form
Mon, 26 May 1997 12:40:51 +0200 paulson Deleted option_case_tac because exhaust_tac performs a similar function.
Thu, 22 May 1997 15:09:09 +0200 paulson Deleted obsolete proofs. But option_case_tac will be obsolete too
Fri, 11 Apr 1997 15:21:36 +0200 paulson Yet more fast_tac->blast_tac, and other tidying
Mon, 07 Oct 1996 10:28:44 +0200 paulson Removed commands made redundant by new one-point rules
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Tue, 24 Sep 1996 09:02:34 +0200 nipkow Moved Option out of IOA into core HOL
less more (0) tip