| Wed, 14 Dec 1994 11:17:18 +0100 |
clasohm |
added bind_thm for theorems made by "standard ..."
Isabelle94-2
|
file |
diff |
annotate
|
| Fri, 25 Nov 1994 09:12:16 +0100 |
clasohm |
replaced prove_goal by qed_goal
|
file |
diff |
annotate
|
| Mon, 21 Nov 1994 17:50:34 +0100 |
clasohm |
replaced 'val ... = result()' by 'qed "..."'
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 11:15:01 +0200 |
lcp |
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
|
file |
diff |
annotate
|
| Thu, 18 Aug 1994 11:43:40 +0200 |
lcp |
HOL/Sum: rotated arguments of sum_case; added translation for case macro
|
file |
diff |
annotate
|
| Wed, 26 Jan 1994 17:53:27 +0100 |
nipkow |
sum: renamed case to sum_case
|
file |
diff |
annotate
|
| Thu, 07 Oct 1993 10:20:30 +0100 |
lcp |
added ~= for "not equals" and added ~: for "not in"
|
file |
diff |
annotate
|
| Wed, 22 Sep 1993 15:43:05 +0200 |
lcp |
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|