| Wed, 14 Apr 2004 14:13:05 +0200 |
use more symbols in HTML output
|
file | diff | annotate |
| Tue, 20 Jan 2004 13:56:27 +0100 |
Added print translation for pairs
|
file | diff | annotate |
| Mon, 05 Jan 2004 00:46:06 +0100 |
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
|
file | diff | annotate |
| Fri, 26 Sep 2003 10:34:57 +0200 |
misc tidying
|
file | diff | annotate |
| Mon, 15 Sep 2003 14:00:43 +0200 |
Fixed blunder in the setup of the classical reasoner wrt. the constant
|
file | diff | annotate |
| Mon, 15 Sep 2003 12:27:13 +0200 |
Added the constant "curry".
|
file | diff | annotate |
| Fri, 11 Jul 2003 14:12:41 +0200 |
added upd_fst, upd_snd, some thms
|
file | diff | annotate |
| Thu, 08 Aug 2002 23:46:09 +0200 |
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
|
file | diff | annotate |
| Tue, 06 Aug 2002 11:22:05 +0200 |
sane interface for simprocs;
|
file | diff | annotate |
| Sat, 01 Dec 2001 18:52:32 +0100 |
renamed class "term" to "type" (actually "HOL.type");
|
file | diff | annotate |
| Fri, 09 Nov 2001 00:09:47 +0100 |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file | diff | annotate |
| Sat, 27 Oct 2001 23:16:15 +0200 |
tuned;
|
file | diff | annotate |
| Fri, 19 Oct 2001 22:01:25 +0200 |
got rid of ML proof scripts for Product_Type;
|
file | diff | annotate |
| Wed, 17 Oct 2001 20:24:03 +0200 |
proper proof of split_paired_all (presently unused);
|
file | diff | annotate |
| Mon, 15 Oct 2001 20:33:42 +0200 |
tuned;
|
file | diff | annotate |
| Thu, 27 Sep 2001 22:22:58 +0200 |
renamed "()" to Unity, made local;
|
file | diff | annotate |
| Thu, 09 Aug 2001 10:17:45 +0200 |
added pair_imageI (also as intro rule)
|
file | diff | annotate |
| Wed, 25 Jul 2001 13:13:01 +0200 |
partial restructuring to reduce dependence on Axiom of Choice
|
file | diff | annotate |
| Sun, 15 Jul 2001 14:47:28 +0200 |
tuned;
|
file | diff | annotate |
| Fri, 02 Feb 2001 22:18:10 +0100 |
added hidden internal_split constant;
|
file | diff | annotate |
| Thu, 01 Feb 2001 20:51:48 +0100 |
converted to Isar therory, adding attributes complete_split and split_format
|
file | diff | annotate |
| Mon, 23 Oct 2000 11:14:00 +0200 |
tuned deps;
|
file | diff | annotate |
| Thu, 12 Oct 2000 18:44:35 +0200 |
*** empty log message ***
|
file | diff | annotate |