wenzelm [Sun, 11 Nov 2007 16:58:41 +0100] rev 25401
updated;
wenzelm [Sun, 11 Nov 2007 16:50:30 +0100] rev 25400
auto quickcheck: reduced messages;
wenzelm [Sun, 11 Nov 2007 16:50:29 +0100] rev 25399
notation works with any known constant (including fixes/abbrevs);
wenzelm [Sun, 11 Nov 2007 16:50:27 +0100] rev 25398
HOL-Statespace;
wenzelm [Sun, 11 Nov 2007 16:45:47 +0100] rev 25397
* HOL-Statespace;
wenzelm [Sun, 11 Nov 2007 16:24:22 +0100] rev 25396
restore interrupt handler on init;
wenzelm [Sun, 11 Nov 2007 14:17:15 +0100] rev 25395
abbrev: back to PrintMode.internal, which works at least half-way;
wenzelm [Sun, 11 Nov 2007 14:00:13 +0100] rev 25394
syntax operations: turned extend'' into update'' (absorb duplicates);
tuned signature;
wenzelm [Sun, 11 Nov 2007 14:00:12 +0100] rev 25393
replaced extend_prtabs by update_prtabs (absorb duplicates);
wenzelm [Sun, 11 Nov 2007 14:00:11 +0100] rev 25392
abbrev: PrintMode.input instead of PrintMode.internal for global version!
wenzelm [Sun, 11 Nov 2007 14:00:10 +0100] rev 25391
renamed update_list to cons_list;
added proper update_list (based on Library.update);
wenzelm [Sun, 11 Nov 2007 14:00:09 +0100] rev 25390
syntax operations: turned extend'' into update'' (absorb duplicates);
wenzelm [Sun, 11 Nov 2007 14:00:08 +0100] rev 25389
renamed Symtab.update_list to Symtab.cons_list;
wenzelm [Sun, 11 Nov 2007 14:00:05 +0100] rev 25388
tuned specifications of 'notation';
wenzelm [Sat, 10 Nov 2007 23:04:03 +0100] rev 25387
added update_const_gram (avoids duplicates);
tuned;
wenzelm [Sat, 10 Nov 2007 23:04:02 +0100] rev 25386
remove_prtabs: tuned, avoid excessive garbage;
wenzelm [Sat, 10 Nov 2007 23:04:00 +0100] rev 25385
update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);
wenzelm [Sat, 10 Nov 2007 23:03:57 +0100] rev 25384
similar_types: uniform treatment of TFrees/TVars;
wenzelm [Sat, 10 Nov 2007 23:03:56 +0100] rev 25383
notation: based on Syntax.update_const_gram (avoids duplicates);
wenzelm [Sat, 10 Nov 2007 23:03:52 +0100] rev 25382
tuned specifications of 'notation';
wenzelm [Sat, 10 Nov 2007 18:36:10 +0100] rev 25381
removed LocalTheory.target_naming/name;
wenzelm [Sat, 10 Nov 2007 18:36:08 +0100] rev 25380
put_inductives: be permissive about multiple versions
(target names are not necessarily unique);
add_inductive: store info under global (!) name -- very rough approximation of the real thing;
wenzelm [Sat, 10 Nov 2007 18:36:07 +0100] rev 25379
tuned proofs;
tuned document;
wenzelm [Sat, 10 Nov 2007 18:36:06 +0100] rev 25378
tuned document;
wenzelm [Sat, 10 Nov 2007 18:36:06 +0100] rev 25377
Orderings.min/max: no need to qualify consts;
removed legacy ML bindings;
wenzelm [Sat, 10 Nov 2007 15:58:18 +0100] rev 25376
auto_quickcheck ref: set default in ProofGeneral/preferences only
(retains responsiveness of plain tty interaction);
auto_quickcheck: more messages, less complicated code;
wenzelm [Sat, 10 Nov 2007 15:58:18 +0100] rev 25375
ProofGeneral/preferences: auto_quickcheck=true;
wenzelm [Sat, 10 Nov 2007 14:36:33 +0100] rev 25374
qualified Proofterm.proofs;
wenzelm [Sat, 10 Nov 2007 14:31:23 +0100] rev 25373
@{const}: improved ProofContext.read_const does the job;
wenzelm [Sat, 10 Nov 2007 14:31:22 +0100] rev 25372
locale_const: suppress in class body as well (prevents qualified printing);
wenzelm [Sat, 10 Nov 2007 14:31:21 +0100] rev 25371
notation: improved ProofContext.read_const does the job;
wenzelm [Sat, 10 Nov 2007 14:31:20 +0100] rev 25370
updated;
wenzelm [Sat, 10 Nov 2007 14:31:18 +0100] rev 25369
replaced @{const} (allows name only) by proper @{term};
haftmann [Fri, 09 Nov 2007 23:24:31 +0100] rev 25368
proper implementation of check phase; non-qualified names for class operations
haftmann [Fri, 09 Nov 2007 23:24:30 +0100] rev 25367
explicit message for failed autoquickcheck
wenzelm [Fri, 09 Nov 2007 19:37:35 +0100] rev 25366
tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;
wenzelm [Fri, 09 Nov 2007 19:37:35 +0100] rev 25365
avoid obsolete Sign.read_prop;
wenzelm [Fri, 09 Nov 2007 19:37:33 +0100] rev 25364
tuned proofs -- avoid implicit prems;
wenzelm [Fri, 09 Nov 2007 19:37:32 +0100] rev 25363
fixed imports path;
wenzelm [Fri, 09 Nov 2007 19:37:30 +0100] rev 25362
tuned proofs -- avoid open cases;
krauss [Fri, 09 Nov 2007 18:59:56 +0100] rev 25361
function package: using the names of the equations as case names turned out to be impractical => disabled
krauss [Fri, 09 Nov 2007 13:41:27 +0100] rev 25360
avoid name clashes when generating code for union, inter
wenzelm [Thu, 08 Nov 2007 22:57:45 +0100] rev 25359
oops -- avoid vacous goal message;
tuned messages;
wenzelm [Thu, 08 Nov 2007 22:36:46 +0100] rev 25358
tuned messages;
tuned;
wenzelm [Thu, 08 Nov 2007 22:19:43 +0100] rev 25357
avoid "import" as identifier, which is a keyword in Alice;
wenzelm [Thu, 08 Nov 2007 20:52:27 +0100] rev 25356
tuned presentation;
wenzelm [Thu, 08 Nov 2007 20:09:17 +0100] rev 25355
avoid implicit use of prems;
tuned proofs;
wenzelm [Thu, 08 Nov 2007 20:08:11 +0100] rev 25354
where/of: do not allow schematic variables here!
wenzelm [Thu, 08 Nov 2007 20:08:09 +0100] rev 25353
removed unused read_termTs_schematic, read/cert_vars_legacy, add_fixes_legacy;
discontinued legacy_intern_skolem, gen_read';
wenzelm [Thu, 08 Nov 2007 20:08:07 +0100] rev 25352
discontinued legacy vars;
wenzelm [Thu, 08 Nov 2007 20:08:02 +0100] rev 25351
removed unused read_def_terms';
wenzelm [Thu, 08 Nov 2007 20:08:01 +0100] rev 25350
eliminated illegal schematic variables in where/of;
wenzelm [Thu, 08 Nov 2007 20:08:00 +0100] rev 25349
eliminated illegal schematic variables in where/of;
tuned;
wenzelm [Thu, 08 Nov 2007 20:07:58 +0100] rev 25348
x86_64: fall back on x86 (more efficient);
wenzelm [Thu, 08 Nov 2007 20:07:57 +0100] rev 25347
tuned comments;
wenzelm [Thu, 08 Nov 2007 14:51:31 +0100] rev 25346
renamed ProofContext.read_const' to ProofContext.read_const_proper;