| Mon, 10 Oct 2005 04:03:09 +0200 |
huffman |
cleaned up
|
changeset |
files
|
| Mon, 10 Oct 2005 04:00:40 +0200 |
huffman |
added theorem typedef_chfin
|
changeset |
files
|
| Mon, 10 Oct 2005 03:55:39 +0200 |
huffman |
replaced foldr' with foldr1
|
changeset |
files
|
| Mon, 10 Oct 2005 03:47:00 +0200 |
huffman |
cleaned up; renamed "Porder.op <<" to "Porder.<<"
|
changeset |
files
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
changeset |
files
|
| Sat, 08 Oct 2005 23:43:15 +0200 |
wenzelm |
tuned Memory.hilim;
|
changeset |
files
|
| Sat, 08 Oct 2005 23:43:14 +0200 |
wenzelm |
get rid of feeder -- at the cost of batch-only commit-at-exit;
|
changeset |
files
|
| Sat, 08 Oct 2005 23:36:01 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Sat, 08 Oct 2005 23:05:59 +0200 |
wenzelm |
-nort option;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:42 +0200 |
wenzelm |
added could_unify;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:41 +0200 |
wenzelm |
more efficient check_specified, much less invocations;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:40 +0200 |
wenzelm |
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:39 +0200 |
wenzelm |
uses susp.ML, lazy_seq.ML, lazy_scan.ML;
|
changeset |
files
|
| Sat, 08 Oct 2005 22:39:38 +0200 |
wenzelm |
added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:38 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:37 +0200 |
wenzelm |
tuned memory limits;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:36 +0200 |
wenzelm |
Int.max;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:35 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:34 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:33 +0200 |
wenzelm |
initial pop11 code for ML use/use_string;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:32 +0200 |
wenzelm |
Poplog/PML: ML_SUFFIX=.psv;
|
changeset |
files
|
| Sat, 08 Oct 2005 20:15:31 +0200 |
wenzelm |
support ML_SUFFIX;
|
changeset |
files
|
| Sat, 08 Oct 2005 18:51:03 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sat, 08 Oct 2005 15:20:58 +0200 |
nipkow |
fix due to new neq_simproc
|
changeset |
files
|
| Fri, 07 Oct 2005 23:29:00 +0200 |
wenzelm |
removed obsolete comment;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:26 +0200 |
wenzelm |
added idtypdummy_ast_tr;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:25 +0200 |
wenzelm |
added syntax for _idtdummy, _idtypdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:24 +0200 |
wenzelm |
added absdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:23 +0200 |
wenzelm |
removed obsolete dummy_pat_tr;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:22 +0200 |
wenzelm |
Term.absdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:21 +0200 |
wenzelm |
removed obsolete ex/Tuple.thy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:19 +0200 |
wenzelm |
replaced _K by dummy abstraction;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:18 +0200 |
wenzelm |
print_translation: does not handle _idtdummy;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 07 Oct 2005 22:59:15 +0200 |
wenzelm |
added dummy variable binding;
|
changeset |
files
|
| Fri, 07 Oct 2005 20:41:10 +0200 |
nipkow |
changes due to new neq_simproc in simpdata.ML
|
changeset |
files
|
| Fri, 07 Oct 2005 18:49:20 +0200 |
wenzelm |
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
|
changeset |
files
|
| Fri, 07 Oct 2005 18:49:19 +0200 |
wenzelm |
Term.str_of_term;
|
changeset |
files
|
| Fri, 07 Oct 2005 17:57:21 +0200 |
paulson |
minor code tidyig
|
changeset |
files
|
| Fri, 07 Oct 2005 15:08:28 +0200 |
paulson |
code restructuring
|
changeset |
files
|
| Fri, 07 Oct 2005 11:29:24 +0200 |
paulson |
more tidying. Fixed process management bugs and race condition
|
changeset |
files
|
| Thu, 06 Oct 2005 10:14:22 +0200 |
paulson |
major simplification: removal of the goalstring argument
|
changeset |
files
|
| Thu, 06 Oct 2005 10:13:34 +0200 |
berghofe |
Optimized getPreds and getSuccs.
|
changeset |
files
|
| Thu, 06 Oct 2005 08:58:58 +0200 |
haftmann |
adjusted sydney to new website
|
changeset |
files
|
| Thu, 06 Oct 2005 08:56:15 +0200 |
haftmann |
changed sydney share
|
changeset |
files
|
| Wed, 05 Oct 2005 19:28:12 +0200 |
wenzelm |
added Poplog/PML version 15.6/2.1 (experimental!);
|
changeset |
files
|
| Wed, 05 Oct 2005 18:38:43 +0200 |
haftmann |
added fold_nodes, map_node_yield
|
changeset |
files
|
| Wed, 05 Oct 2005 18:38:28 +0200 |
haftmann |
added merge, tuned
|
changeset |
files
|
| Wed, 05 Oct 2005 14:01:32 +0200 |
nipkow |
added last in set lemma
|
changeset |
files
|
| Wed, 05 Oct 2005 11:18:06 +0200 |
paulson |
improved process handling. tidied
|
changeset |
files
|
| Wed, 05 Oct 2005 10:56:06 +0200 |
paulson |
more signals
|
changeset |
files
|
| Tue, 04 Oct 2005 23:39:42 +0200 |
nipkow |
new hd/rev/last lemmas
|
changeset |
files
|
| Tue, 04 Oct 2005 23:30:46 +0200 |
nipkow |
new lemmas
|
changeset |
files
|
| Tue, 04 Oct 2005 21:39:16 +0200 |
wenzelm |
added compiler and runtime options;
|
changeset |
files
|
| Tue, 04 Oct 2005 21:33:09 +0200 |
wenzelm |
Poplog/PML startup script.
|
changeset |
files
|
| Tue, 04 Oct 2005 20:38:13 +0200 |
wenzelm |
Compatibility file for Poplog/PML (version 15.6/2.1).
|
changeset |
files
|
| Tue, 04 Oct 2005 19:05:37 +0200 |
wenzelm |
Substring.all = Substring.full;
|
changeset |
files
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
changeset |
files
|
| Tue, 04 Oct 2005 16:47:40 +0200 |
wenzelm |
find_theorems: support * wildcard in name: criterion;
|
changeset |
files
|
| Tue, 04 Oct 2005 16:47:39 +0200 |
wenzelm |
* Command 'find_theorems': support * wildcard in name: criterion.
|
changeset |
files
|