nipkow [Thu, 13 Dec 2001 19:05:10 +0100] rev 12492
*** empty log message ***
nipkow [Thu, 13 Dec 2001 17:57:55 +0100] rev 12491
*** empty log message ***
wenzelm [Thu, 13 Dec 2001 17:44:56 +0100] rev 12490
made SML/XL happy;
nipkow [Thu, 13 Dec 2001 16:48:34 +0100] rev 12489
*** empty log message ***
nipkow [Thu, 13 Dec 2001 16:48:07 +0100] rev 12488
Terminator now uses arith_tac as well.
nipkow [Thu, 13 Dec 2001 16:47:35 +0100] rev 12487
comp -> rel_comp
wenzelm [Thu, 13 Dec 2001 15:45:03 +0100] rev 12486
isatool expandshort;
paulson [Thu, 13 Dec 2001 12:33:23 +0100] rev 12485
Relaxed the precondition of UN_upper_le
wenzelm [Wed, 12 Dec 2001 20:37:31 +0100] rev 12484
isatool expandshort;
nipkow [Wed, 12 Dec 2001 19:22:21 +0100] rev 12483
new rewrite rules for use by arith_tac to take care of uminus.
mods due to reorienting and renaming of real_minus_mult_eq1/2
nipkow [Wed, 12 Dec 2001 19:21:54 +0100] rev 12482
new rewrite rules for use by arith_tac to take care of uminus.
nipkow [Wed, 12 Dec 2001 19:21:02 +0100] rev 12481
mods due to reorienting and renaming of real_minus_mult_eq1/2
nipkow [Wed, 12 Dec 2001 19:19:59 +0100] rev 12480
tuned conversion from terms to "polynomials" for arith_tac: takes care
of "uminus" now.
wenzelm [Wed, 12 Dec 2001 18:05:44 +0100] rev 12479
drop_judgment: be graceful about undeclared judgment;
wenzelm [Wed, 12 Dec 2001 18:03:10 +0100] rev 12478
obsolete;
wenzelm [Wed, 12 Dec 2001 17:43:45 +0100] rev 12477
option "-d pdf" by default (accomodates pdf bias of Mac OS X);
tuned getpwnam;
wenzelm [Wed, 12 Dec 2001 17:40:36 +0100] rev 12476
removed installfonts, xterm interface;
improved default of PROOFGENERAL_OPTIONS;
nipkow [Wed, 12 Dec 2001 12:40:02 +0100] rev 12475
Removed pointless backtracking from arith_tac
berghofe [Wed, 12 Dec 2001 11:07:42 +0100] rev 12474
Improved error messages.
nipkow [Wed, 12 Dec 2001 09:04:20 +0100] rev 12473
*** empty log message ***
wenzelm [Tue, 11 Dec 2001 17:07:45 +0100] rev 12472
tuned;
wenzelm [Tue, 11 Dec 2001 17:02:46 +0100] rev 12471
obsolete;
wenzelm [Tue, 11 Dec 2001 16:44:43 +0100] rev 12470
obsolete;
wenzelm [Tue, 11 Dec 2001 16:25:31 +0100] rev 12469
tuned;
wenzelm [Tue, 11 Dec 2001 16:22:44 +0100] rev 12468
\isasymindex made text mode;
wenzelm [Tue, 11 Dec 2001 16:22:09 +0100] rev 12467
isatools "symbolinput" and "nonascii" have disappeared;
wenzelm [Tue, 11 Dec 2001 16:00:26 +0100] rev 12466
added HOL-Library;
wenzelm [Tue, 11 Dec 2001 15:58:32 +0100] rev 12465
tuned;
wenzelm [Tue, 11 Dec 2001 15:36:28 +0100] rev 12464
updated;
wenzelm [Tue, 11 Dec 2001 15:04:17 +0100] rev 12463
removed altogether;
wenzelm [Tue, 11 Dec 2001 15:03:57 +0100] rev 12462
removed unused stuff;
berghofe [Tue, 11 Dec 2001 14:54:18 +0100] rev 12461
Updated.
wenzelm [Tue, 11 Dec 2001 13:43:00 +0100] rev 12460
oops;
wenzelm [Mon, 10 Dec 2001 20:59:43 +0100] rev 12459
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm [Mon, 10 Dec 2001 20:58:15 +0100] rev 12458
updated reserved words of HOL;
wenzelm [Mon, 10 Dec 2001 20:57:44 +0100] rev 12457
* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
of "lam" -- INCOMPATIBILITY;
wenzelm [Mon, 10 Dec 2001 19:14:56 +0100] rev 12456
obsolete;
wenzelm [Mon, 10 Dec 2001 18:52:15 +0100] rev 12455
removed additional blank line (confuses some versions of make);
wenzelm [Mon, 10 Dec 2001 18:50:01 +0100] rev 12454
obsolete;
berghofe [Mon, 10 Dec 2001 15:40:55 +0100] rev 12453
- Changed type of invoke_codegen
- Added combinators for sequences
berghofe [Mon, 10 Dec 2001 15:39:34 +0100] rev 12452
- Added code generator interface for types
- Changed type of invoke_codegen
berghofe [Mon, 10 Dec 2001 15:37:03 +0100] rev 12451
Fixed bug in function find_paths.
berghofe [Mon, 10 Dec 2001 15:36:05 +0100] rev 12450
Added example file for intuitionistic logic (taken from FOL).
berghofe [Mon, 10 Dec 2001 15:35:03 +0100] rev 12449
Added support for code generation.
berghofe [Mon, 10 Dec 2001 15:34:15 +0100] rev 12448
Recursive equations to be used for code generation are now registered
via RecfunCodegen.add
berghofe [Mon, 10 Dec 2001 15:32:10 +0100] rev 12447
Code generator for recursive functions.
berghofe [Mon, 10 Dec 2001 15:31:30 +0100] rev 12446
Tuned header.
berghofe [Mon, 10 Dec 2001 15:30:18 +0100] rev 12445
Code generator for datatypes.
berghofe [Mon, 10 Dec 2001 15:29:16 +0100] rev 12444
Moved contents to files datatype_codegen.ML and recfun_codegen.ML
berghofe [Mon, 10 Dec 2001 15:26:42 +0100] rev 12443
Turned subcls1 into an inductive relation to make it executable.
berghofe [Mon, 10 Dec 2001 15:24:48 +0100] rev 12442
Example for code generator.
berghofe [Mon, 10 Dec 2001 15:24:22 +0100] rev 12441
Added examples for code generator.
berghofe [Mon, 10 Dec 2001 15:23:19 +0100] rev 12440
Added code generator setup.
berghofe [Mon, 10 Dec 2001 15:18:57 +0100] rev 12439
Tuned code generator setup.
berghofe [Mon, 10 Dec 2001 15:18:34 +0100] rev 12438
Added new files (code generator and examples).
berghofe [Mon, 10 Dec 2001 15:17:49 +0100] rev 12437
Moved code generator setup from Recdef to Inductive.
berghofe [Mon, 10 Dec 2001 15:16:49 +0100] rev 12436
Replaced several occurrences of "blast" by "rules".
wenzelm [Mon, 10 Dec 2001 13:30:14 +0100] rev 12435
document root;
kleing [Sun, 09 Dec 2001 15:26:13 +0100] rev 12434
tuned
kleing [Sun, 09 Dec 2001 14:37:42 +0100] rev 12433
HOLCF/IMP converted to Isar