| Mon, 04 Oct 1999 14:45:35 +0200 |
wenzelm |
added mk_conj, mk_disj, mk_imp;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 14:13:45 +0200 |
nipkow |
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
|
file |
diff |
annotate
|
| Tue, 03 Aug 1999 13:15:20 +0200 |
paulson |
added realT
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 17:25:27 +0200 |
paulson |
added boolean and binary constants
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 13:46:23 +0100 |
wenzelm |
added dest_mem;
|
file |
diff |
annotate
|
| Fri, 18 Dec 1998 11:00:15 +0100 |
paulson |
new function dest_eq
|
file |
diff |
annotate
|
| Tue, 28 Jul 1998 16:59:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 30 Jun 1998 20:41:41 +0200 |
berghofe |
Moved most of the Prod_Syntax - stuff to HOLogic.
|
file |
diff |
annotate
|
| Wed, 14 Jan 1998 10:30:44 +0100 |
wenzelm |
added unit and prod stuff;
|
file |
diff |
annotate
|
| Tue, 23 Dec 1997 11:39:03 +0100 |
paulson |
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
|
file |
diff |
annotate
|
| Wed, 26 Nov 1997 16:43:42 +0100 |
wenzelm |
added dest_nat;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 19:15:02 +0200 |
wenzelm |
eliminated raise_term, raise_typ;
|
file |
diff |
annotate
|
| Thu, 16 Jan 1997 16:53:15 +0100 |
wenzelm |
binary oprations and relations;
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|