Fri, 31 Mar 2000 10:17:32 +0200 |
kleing |
tuned
|
changeset |
files
|
Fri, 31 Mar 2000 10:15:33 +0200 |
kleing |
included new stanford mirror, mirror links now point to source directly
|
changeset |
files
|
Fri, 31 Mar 2000 10:08:26 +0200 |
nipkow |
updated recdef
|
changeset |
files
|
Thu, 30 Mar 2000 21:26:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 30 Mar 2000 20:06:27 +0200 |
nipkow |
recdef
|
changeset |
files
|
Thu, 30 Mar 2000 19:47:17 +0200 |
nipkow |
If all termination conditions are proved automatically,
|
changeset |
files
|
Thu, 30 Mar 2000 19:45:51 +0200 |
nipkow |
recdef.rules -> recdef.simps
|
changeset |
files
|
Thu, 30 Mar 2000 19:45:18 +0200 |
nipkow |
mod in recdef allows to access the correct simpset via simpset().
|
changeset |
files
|
Thu, 30 Mar 2000 19:44:11 +0200 |
nipkow |
the simplification rules returned from TFL are now paired with the row they
|
changeset |
files
|
Thu, 30 Mar 2000 15:13:59 +0200 |
wenzelm |
* Isar/Pure: local results and corresponding term bindings are now
|
changeset |
files
|
Thu, 30 Mar 2000 15:13:02 +0200 |
wenzelm |
support Hindley-Milner polymorphisms in results and bindings;
|
changeset |
files
|
Thu, 30 Mar 2000 15:12:20 +0200 |
wenzelm |
added 'moreover' and 'ultimately';
|
changeset |
files
|
Thu, 30 Mar 2000 15:11:48 +0200 |
wenzelm |
added \MOREOVER, \ULTIMATELY;
|
changeset |
files
|
Thu, 30 Mar 2000 14:28:54 +0200 |
wenzelm |
support Hindley-Milner polymorphisms in binds and facts;
|
changeset |
files
|
Thu, 30 Mar 2000 14:28:10 +0200 |
wenzelm |
support Hindley-Milner polymorphisms in binds and facts;
|
changeset |
files
|
Thu, 30 Mar 2000 14:25:35 +0200 |
wenzelm |
let_bind(_i): polymorphic version;
|
changeset |
files
|
Thu, 30 Mar 2000 14:24:46 +0200 |
wenzelm |
ProofContext.find_free;
|
changeset |
files
|
Thu, 30 Mar 2000 14:22:15 +0200 |
wenzelm |
'tactic': refer to PureIsar structure;
|
changeset |
files
|
Thu, 30 Mar 2000 14:21:28 +0200 |
wenzelm |
?this: support params;
|
changeset |
files
|
Thu, 30 Mar 2000 14:20:42 +0200 |
wenzelm |
support polymorphic Vars;
|
changeset |
files
|
Thu, 30 Mar 2000 14:20:13 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Thu, 30 Mar 2000 14:20:01 +0200 |
wenzelm |
foldl_term_types: depend on term as well;
|
changeset |
files
|
Thu, 30 Mar 2000 14:19:33 +0200 |
wenzelm |
read_def_cterms: use Sign.read_def_terms;
|
changeset |
files
|
Thu, 30 Mar 2000 14:19:13 +0200 |
wenzelm |
read_def_terms (no certify yet);
|
changeset |
files
|
Thu, 30 Mar 2000 14:18:40 +0200 |
wenzelm |
export update_multi;
|
changeset |
files
|
Thu, 30 Mar 2000 14:15:41 +0200 |
wenzelm |
added tvars_intr_list;
|
changeset |
files
|
Wed, 29 Mar 2000 15:09:51 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Wed, 29 Mar 2000 14:23:27 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
Tue, 28 Mar 2000 17:33:44 +0200 |
nipkow |
mods because of weak_case_cong -> removed Action.ML twice
|
changeset |
files
|
Tue, 28 Mar 2000 17:32:24 +0200 |
nipkow |
added weak_case_cong feature
|
changeset |
files
|
Tue, 28 Mar 2000 17:31:36 +0200 |
nipkow |
mods because of weak_case_cong
|
changeset |
files
|
Tue, 28 Mar 2000 12:28:24 +0200 |
wenzelm |
fixed railqtoken;
|
changeset |
files
|
Tue, 28 Mar 2000 11:50:23 +0200 |
wenzelm |
-I option;
|
changeset |
files
|
Mon, 27 Mar 2000 21:41:19 +0200 |
wenzelm |
renamed 'hoare_vcg' to 'hoare';
|
changeset |
files
|
Mon, 27 Mar 2000 21:13:23 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Mon, 27 Mar 2000 21:13:06 +0200 |
wenzelm |
fixed dddot_tr;
|
changeset |
files
|
Mon, 27 Mar 2000 18:10:11 +0200 |
wenzelm |
rail token vs. terminal;
|
changeset |
files
|
Mon, 27 Mar 2000 18:09:49 +0200 |
wenzelm |
fixed term syntax;
|
changeset |
files
|
Mon, 27 Mar 2000 18:09:24 +0200 |
wenzelm |
tail token vs. terminal;
|
changeset |
files
|
Mon, 27 Mar 2000 18:08:57 +0200 |
wenzelm |
fixed \rail@tokenfont (ever used?);
|
changeset |
files
|
Mon, 27 Mar 2000 17:04:03 +0200 |
paulson |
added an order-sorted version of quickSort
|
changeset |
files
|
Mon, 27 Mar 2000 16:25:53 +0200 |
paulson |
simplified constant "colored"
|
changeset |
files
|
Sun, 26 Mar 2000 22:31:11 +0200 |
wenzelm |
added 'ultimately';
|
changeset |
files
|
Sun, 26 Mar 2000 22:29:33 +0200 |
wenzelm |
added WhileRule';
|
changeset |
files
|
Sun, 26 Mar 2000 20:38:23 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
Sun, 26 Mar 2000 20:17:52 +0200 |
wenzelm |
tuned presentation;
|
changeset |
files
|
Sun, 26 Mar 2000 20:16:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Sun, 26 Mar 2000 20:13:53 +0200 |
wenzelm |
ignore_stuff;
|
changeset |
files
|
Sun, 26 Mar 2000 20:12:28 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
Sun, 26 Mar 2000 20:11:12 +0200 |
wenzelm |
!!!! = cut "Corrupted outer syntax in presentation";
|
changeset |
files
|
Sun, 26 Mar 2000 20:10:31 +0200 |
wenzelm |
added is_begin/end_ignore;
|
changeset |
files
|
Sun, 26 Mar 2000 20:08:03 +0200 |
wenzelm |
tuned targets;
|
changeset |
files
|
Sat, 25 Mar 2000 18:01:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
Sat, 25 Mar 2000 17:59:52 +0100 |
wenzelm |
improved (anti)quote_tr(');
|
changeset |
files
|
Sat, 25 Mar 2000 13:00:44 +0100 |
wenzelm |
addsimprocs [record_simproc];
|
changeset |
files
|
Sat, 25 Mar 2000 12:59:31 +0100 |
wenzelm |
tuned antiquote_tr';
|
changeset |
files
|
Sat, 25 Mar 2000 12:52:06 +0100 |
wenzelm |
export updateN;
|
changeset |
files
|
Fri, 24 Mar 2000 21:15:56 +0100 |
wenzelm |
use abstract syntax;
|
changeset |
files
|
Fri, 24 Mar 2000 21:09:34 +0100 |
wenzelm |
plain ASCII;
|
changeset |
files
|
Fri, 24 Mar 2000 20:59:15 +0100 |
wenzelm |
arith method: HEADGOAL;
|
changeset |
files
|