Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
Fri, 14 Jul 2000 16:28:58 +0200 |
oheimb |
added option_map_o_sum_case (also to simpset)
|
file |
diff |
annotate
|
Tue, 30 May 2000 18:02:49 +0200 |
berghofe |
the is now defined using primrec, avoiding explicit use of arbitrary.
|
file |
diff |
annotate
|
Mon, 13 Mar 2000 16:23:34 +0100 |
wenzelm |
case_tac now subsumes both boolean and datatype cases;
|
file |
diff |
annotate
|
Mon, 13 Mar 2000 12:51:10 +0100 |
nipkow |
exhaust_tac -> cases_tac
|
file |
diff |
annotate
|
Mon, 19 Jul 1999 15:19:11 +0200 |
paulson |
getting rid of qed_goal
|
file |
diff |
annotate
|
Mon, 21 Sep 1998 23:06:37 +0200 |
oheimb |
added addD2, addE2, addSD2, and addSE2
|
file |
diff |
annotate
|
Wed, 09 Sep 1998 17:23:42 +0200 |
oheimb |
AddIffs[not_None_eq];
|
file |
diff |
annotate
|
Wed, 12 Aug 1998 15:00:46 +0200 |
oheimb |
added ospec
|
file |
diff |
annotate
|
Fri, 24 Jul 1998 13:03:20 +0200 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
Mon, 27 Apr 1998 19:29:19 +0200 |
oheimb |
added option_map_eq_Some via AddIffs
|
file |
diff |
annotate
|
Tue, 07 Apr 1998 13:46:05 +0200 |
oheimb |
replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
|
file |
diff |
annotate
|
Tue, 24 Mar 1998 15:51:37 +0100 |
oheimb |
added o2s
|
file |
diff |
annotate
|
Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
file |
diff |
annotate
|
Tue, 04 Nov 1997 20:48:38 +0100 |
oheimb |
added the, option_map, and case analysis theorems
|
file |
diff |
annotate
|
Mon, 03 Nov 1997 09:57:35 +0100 |
nipkow |
expand_option_case -> split_option_case
|
file |
diff |
annotate
|
Thu, 30 Oct 1997 09:45:03 +0100 |
nipkow |
For each datatype `t' there is now a theorem `split_t_case' of the form
|
file |
diff |
annotate
|
Mon, 26 May 1997 12:40:51 +0200 |
paulson |
Deleted option_case_tac because exhaust_tac performs a similar function.
|
file |
diff |
annotate
|
Thu, 22 May 1997 15:09:09 +0200 |
paulson |
Deleted obsolete proofs. But option_case_tac will be obsolete too
|
file |
diff |
annotate
|
Fri, 11 Apr 1997 15:21:36 +0200 |
paulson |
Yet more fast_tac->blast_tac, and other tidying
|
file |
diff |
annotate
|
Mon, 07 Oct 1996 10:28:44 +0200 |
paulson |
Removed commands made redundant by new one-point rules
|
file |
diff |
annotate
|
Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
Tue, 24 Sep 1996 09:02:34 +0200 |
nipkow |
Moved Option out of IOA into core HOL
|
file |
diff |
annotate
|