| Tue, 18 Oct 2005 17:59:23 +0200 |
wenzelm |
Simplifier.context/theory_context;
|
changeset |
files
|
| Tue, 18 Oct 2005 17:59:22 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 18 Oct 2005 15:08:38 +0200 |
paulson |
new interface to make_conjecture_clauses
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:25 +0200 |
wenzelm |
* Simplifier: simpset of a running simplification process contains a proof context;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:24 +0200 |
wenzelm |
added type_solver (uses Simplifier.the_context);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:23 +0200 |
wenzelm |
added pos/negDivAlg_induct declarations (from Main.thy);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:22 +0200 |
wenzelm |
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:21 +0200 |
wenzelm |
removed obsolete/experimental context components (superceded by Simplifier.the_context);
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:20 +0200 |
wenzelm |
added set/addloop' for simpset dependent loopers;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:19 +0200 |
wenzelm |
functor: no Simplifier argument;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:18 +0200 |
wenzelm |
change_claset(_of): more abtract interface;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:17 +0200 |
wenzelm |
functor: no Simplifier argument;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:16 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:15 +0200 |
wenzelm |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:13 +0200 |
wenzelm |
change_claset/simpset;
|
changeset |
files
|
| Mon, 17 Oct 2005 23:10:10 +0200 |
wenzelm |
change_claset/simpset;
|
changeset |
files
|
| Mon, 17 Oct 2005 19:19:29 +0200 |
berghofe |
Improved proof of injectivity theorems to make it work on
|
changeset |
files
|
| Mon, 17 Oct 2005 18:34:51 +0200 |
berghofe |
Fixed bug in proof of support theorem (it failed on constructors with no arguments).
|
changeset |
files
|
| Mon, 17 Oct 2005 17:42:24 +0200 |
berghofe |
Implemented proofs for support and freshness theorems.
|
changeset |
files
|
| Mon, 17 Oct 2005 17:40:34 +0200 |
urbanc |
deleted leading space in the definition of fresh
|
changeset |
files
|
| Mon, 17 Oct 2005 12:30:57 +0200 |
berghofe |
Initial revision.
|
changeset |
files
|
| Sat, 15 Oct 2005 00:14:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:09:20 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:09:07 +0200 |
wenzelm |
added ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:15 +0200 |
wenzelm |
more;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:14 +0200 |
wenzelm |
* antiquotations ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:13 +0200 |
wenzelm |
added guess;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:12 +0200 |
wenzelm |
added antiquotations ML_type, ML_struct;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:11 +0200 |
wenzelm |
use perl for test/stat;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:10 +0200 |
wenzelm |
export strip_params;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:09 +0200 |
wenzelm |
note_thmss, read/cert_vars etc.: natural argument order;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:08 +0200 |
wenzelm |
goal statements: before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:07 +0200 |
wenzelm |
added 'guess', which derives the obtained context from the course of reasoning;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:06 +0200 |
wenzelm |
added primitive_text, succeed_text;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:05 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:04 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:03 +0200 |
wenzelm |
added 'guess';
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:01 +0200 |
wenzelm |
added no_facts;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:08:00 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 15 Oct 2005 00:07:59 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 14 Oct 2005 15:34:56 +0200 |
paulson |
signature changes
|
changeset |
files
|
| Fri, 14 Oct 2005 14:36:39 +0200 |
haftmann |
added module rat.ML for rational numbers
|
changeset |
files
|
| Fri, 14 Oct 2005 13:04:38 +0200 |
isatest |
longer time out for test (kleing)
|
changeset |
files
|
| Fri, 14 Oct 2005 11:36:14 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
changeset |
files
|
| Fri, 14 Oct 2005 10:19:50 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
changeset |
files
|
| Thu, 13 Oct 2005 11:58:22 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Wed, 12 Oct 2005 18:17:48 +0200 |
webertj |
counter added to SAT signature
|
changeset |
files
|
| Wed, 12 Oct 2005 17:06:22 +0200 |
webertj |
no proof reconstruction when quick_and_dirty is set
|
changeset |
files
|
| Wed, 12 Oct 2005 10:49:07 +0200 |
paulson |
tidying
|
changeset |
files
|
| Wed, 12 Oct 2005 03:02:18 +0200 |
huffman |
domain package generates compactness lemmas for new constructors
|
changeset |
files
|
| Wed, 12 Oct 2005 03:01:30 +0200 |
huffman |
add ML bindings for compactness lemmas
|
changeset |
files
|
| Wed, 12 Oct 2005 03:01:09 +0200 |
huffman |
added compactness theorems
|
changeset |
files
|
| Wed, 12 Oct 2005 01:43:37 +0200 |
huffman |
added compactness lemmas; cleaned up
|
changeset |
files
|
| Tue, 11 Oct 2005 23:47:29 +0200 |
huffman |
added compactness theorems in locale iso
|
changeset |
files
|
| Tue, 11 Oct 2005 23:27:49 +0200 |
huffman |
added several theorems in locale iso
|
changeset |
files
|
| Tue, 11 Oct 2005 23:27:14 +0200 |
huffman |
added xsymbols syntax for pairs; cleaned up
|
changeset |
files
|
| Tue, 11 Oct 2005 23:23:39 +0200 |
huffman |
added theorem typedef_compact
|
changeset |
files
|
| Tue, 11 Oct 2005 23:22:12 +0200 |
huffman |
rearranged subsections; added theorems expand_cfun_eq, expand_cfun_less
|
changeset |
files
|
| Tue, 11 Oct 2005 23:19:50 +0200 |
huffman |
cleaned up; renamed less_fun to expand_fun_less
|
changeset |
files
|
| Tue, 11 Oct 2005 17:30:00 +0200 |
nipkow |
added hd lemma
|
changeset |
files
|
| Tue, 11 Oct 2005 15:04:11 +0200 |
paulson |
simplifying the treatment of clausification
|
changeset |
files
|
| Tue, 11 Oct 2005 15:03:36 +0200 |
paulson |
simplifying the treatment of nameless theorems
|
changeset |
files
|
| Tue, 11 Oct 2005 14:02:33 +0200 |
wenzelm |
expand: error on undefined/empty env variable;
|
changeset |
files
|
| Tue, 11 Oct 2005 14:02:32 +0200 |
wenzelm |
added assert;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:30:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:08 +0200 |
wenzelm |
added string_of_pid;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:07 +0200 |
wenzelm |
raw symbols: allow non-ASCII chars (e.g. UTF-8);
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:06 +0200 |
wenzelm |
moved string_of_pid to ML-Systems;
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:05 +0200 |
wenzelm |
ML_SUFFIX in targets (experimental);
|
changeset |
files
|
| Tue, 11 Oct 2005 13:28:04 +0200 |
wenzelm |
cleanup backup images;
|
changeset |
files
|
| Mon, 10 Oct 2005 15:35:29 +0200 |
paulson |
small tidy-up of utility functions
|
changeset |
files
|
| Mon, 10 Oct 2005 14:43:45 +0200 |
wenzelm |
updated print_tac;
|
changeset |
files
|
| Mon, 10 Oct 2005 05:46:17 +0200 |
huffman |
add names to infix declarations
|
changeset |
files
|
| Mon, 10 Oct 2005 05:30:02 +0200 |
huffman |
new syntax translations for continuous lambda abstraction
|
changeset |
files
|
| Mon, 10 Oct 2005 04:38:26 +0200 |
huffman |
removed Istrictify; simplified some proofs
|
changeset |
files
|
| Mon, 10 Oct 2005 04:12:31 +0200 |
huffman |
added notion of compactness; shortened proof of adm_disj; reorganized and cleaned up
|
changeset |
files
|
| 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
|
| Tue, 04 Oct 2005 16:05:08 +0200 |
wenzelm |
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
|
changeset |
files
|
| Tue, 04 Oct 2005 14:58:44 +0200 |
haftmann |
added redirect.html
|
changeset |
files
|
| Tue, 04 Oct 2005 14:37:06 +0200 |
haftmann |
better error handling
|
changeset |
files
|
| Tue, 04 Oct 2005 11:15:09 +0200 |
haftmann |
improved linktest
|
changeset |
files
|
| Tue, 04 Oct 2005 10:58:46 +0200 |
haftmann |
removed removed IntFloor
|
changeset |
files
|
| Tue, 04 Oct 2005 10:55:14 +0200 |
haftmann |
fixed broken link
|
changeset |
files
|
| Tue, 04 Oct 2005 10:52:43 +0200 |
haftmann |
fixed broken mailto: link
|
changeset |
files
|
| Tue, 04 Oct 2005 09:59:01 +0200 |
paulson |
fixed the ascii-armouring of goalstring
|
changeset |
files
|
| Tue, 04 Oct 2005 09:58:38 +0200 |
paulson |
reset clause counter
|
changeset |
files
|
| Tue, 04 Oct 2005 09:58:17 +0200 |
paulson |
theorems need names
|
changeset |
files
|
| Tue, 04 Oct 2005 09:19:17 +0200 |
haftmann |
support for setting local permissions
|
changeset |
files
|
| Tue, 04 Oct 2005 08:49:24 +0200 |
haftmann |
improved dependency build
|
changeset |
files
|
| Tue, 04 Oct 2005 08:14:15 +0200 |
haftmann |
added conf/ to .cvsignore
|
changeset |
files
|
| Fri, 30 Sep 2005 18:18:34 +0200 |
aspinall |
Add icon for interface.
Isabelle2005
|
changeset |
files
|
| Fri, 30 Sep 2005 17:54:04 +0200 |
aspinall |
Move welcomemsg and helpdoc to pgip_isar.xml
|
changeset |
files
|
| Fri, 30 Sep 2005 17:52:18 +0200 |
aspinall |
Add helpdocs and welcomemsg here instead of hard wiring in proof_general.ML.
|
changeset |
files
|
| Fri, 30 Sep 2005 17:33:22 +0200 |
aspinall |
Explanatory text
|
changeset |
files
|
| Fri, 30 Sep 2005 17:28:04 +0200 |
aspinall |
Schema files (for information, and validating pgip_isar.xml)
|
changeset |
files
|
| Fri, 30 Sep 2005 17:24:51 +0200 |
aspinall |
Schema for PGIP
|
changeset |
files
|
| Fri, 30 Sep 2005 15:28:43 +0200 |
wenzelm |
pruned notes about Poly/ML;
|
changeset |
files
|
| Fri, 30 Sep 2005 15:17:04 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Fri, 30 Sep 2005 13:47:36 +0200 |
aspinall |
Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
|
changeset |
files
|
| Fri, 30 Sep 2005 11:43:42 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 30 Sep 2005 10:58:11 +0200 |
aspinall |
Fix for guiconfig -> displayconfig element rename
|
changeset |
files
|
| Fri, 30 Sep 2005 09:52:46 +0200 |
paulson |
theorems need names
|
changeset |
files
|
| Thu, 29 Sep 2005 19:37:20 +0200 |
wenzelm |
refer to $PRG instead of (old) rsync-isabelle;
|
changeset |
files
|
| Thu, 29 Sep 2005 18:01:12 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:09:11 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:08:52 +0200 |
wenzelm |
pdfsetup.sty: better not rely on ifpdf.sty;
|
changeset |
files
|
| Thu, 29 Sep 2005 17:02:57 +0200 |
paulson |
simprules need names
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:46 +0200 |
wenzelm |
export debug_bounds;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:45 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:44 +0200 |
wenzelm |
explicit dependencies of SAT vs. Refute;
|
changeset |
files
|
| Thu, 29 Sep 2005 15:50:43 +0200 |
wenzelm |
Isabelle2005 (October 2005);
|
changeset |
files
|
| Thu, 29 Sep 2005 15:31:34 +0200 |
nipkow |
Added a few lemmas
|
changeset |
files
|
| Thu, 29 Sep 2005 12:45:16 +0200 |
paulson |
reduction in tracing files
|
changeset |
files
|
| Thu, 29 Sep 2005 12:45:04 +0200 |
paulson |
improvements for problem generation
|
changeset |
files
|
| Thu, 29 Sep 2005 12:44:25 +0200 |
paulson |
moved concat_with_and to watcher.ML
|
changeset |
files
|
| Thu, 29 Sep 2005 12:43:40 +0200 |
paulson |
a name for empty_not_insert
|
changeset |
files
|
| Thu, 29 Sep 2005 12:33:26 +0200 |
berghofe |
Simplifier now removes flex-flex constraints from theorem returned by prover.
|
changeset |
files
|
| Thu, 29 Sep 2005 12:30:30 +0200 |
berghofe |
Optimized and exported flexflex_unique.
|
changeset |
files
|
| Thu, 29 Sep 2005 01:12:16 +0200 |
wenzelm |
make signature constraint actually work;
|
changeset |
files
|
| Thu, 29 Sep 2005 01:09:39 +0200 |
wenzelm |
activate signature constraints;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:03 +0200 |
wenzelm |
HOL4 image is back;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:02 +0200 |
wenzelm |
tuned default operation: use internal modify;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:01 +0200 |
wenzelm |
abstract_rule: tuned exception msgs;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:59:00 +0200 |
wenzelm |
back to simple 'defs' (cf. revision 1.79 of theory.ML);
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:59 +0200 |
wenzelm |
back to simple 'defs' (cf. revision 1.79);
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:58 +0200 |
wenzelm |
removed revert_bound;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:57 +0200 |
wenzelm |
print_theory: discontinued final consts;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:56 +0200 |
wenzelm |
Theory.add_finals_i;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:55 +0200 |
wenzelm |
more finalconsts;
|
changeset |
files
|
| Thu, 29 Sep 2005 00:58:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 28 Sep 2005 18:50:42 +0200 |
webertj |
pointer to HOL/ex/SAT_Examples.thy added
|
changeset |
files
|
| Wed, 28 Sep 2005 16:58:06 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 28 Sep 2005 15:13:02 +0200 |
wenzelm |
more reliable check for PDF output using ifpdf.sty;
|
changeset |
files
|
| Wed, 28 Sep 2005 14:41:43 +0200 |
webertj |
pre_sat_tac moved towards end of file
|
changeset |
files
|
| Wed, 28 Sep 2005 14:16:34 +0200 |
haftmann |
adjusted www links
|
changeset |
files
|
| Wed, 28 Sep 2005 14:16:12 +0200 |
webertj |
comment fixed
|
changeset |
files
|
| Wed, 28 Sep 2005 13:17:23 +0200 |
obua |
mapped "-->" to "hol4-->"
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:15 +0200 |
wenzelm |
avoid naming existing tags in explanations;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:14 +0200 |
wenzelm |
revert 'defs' advertisement;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:50:13 +0200 |
wenzelm |
revert 'defs' advertisement;
|
changeset |
files
|
| Wed, 28 Sep 2005 11:16:27 +0200 |
paulson |
time limit option; fixed bug concerning first line of ATP output
|
changeset |
files
|
| Wed, 28 Sep 2005 11:15:33 +0200 |
paulson |
streamlined theory; conformance to recent publication
|
changeset |
files
|
| Wed, 28 Sep 2005 11:14:26 +0200 |
paulson |
new lemma
|
changeset |
files
|
| Wed, 28 Sep 2005 09:14:44 +0200 |
haftmann |
better appearance in lynx and netscape4
|
changeset |
files
|
| Wed, 28 Sep 2005 08:57:19 +0200 |
haftmann |
MB instead of KB
|
changeset |
files
|
| Tue, 27 Sep 2005 20:43:39 +0200 |
wenzelm |
renamed packages to download;
|
changeset |
files
|
| Tue, 27 Sep 2005 17:24:27 +0200 |
wenzelm |
more details about incomplete 'defs';
|
changeset |
files
|
| Tue, 27 Sep 2005 17:14:27 +0200 |
wenzelm |
renamed "Packages" to "Download";
|
changeset |
files
|
| Tue, 27 Sep 2005 17:13:11 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:09:46 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:09:46 +0200 |
haftmann |
build bed
|
changeset |
files
|
| Tue, 27 Sep 2005 17:03:54 +0200 |
haftmann |
slight corrections
|
changeset |
files
|
| Tue, 27 Sep 2005 17:01:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 27 Sep 2005 17:01:10 +0200 |
wenzelm |
renamed "Packages" to "Download";
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:38 +0200 |
haftmann |
fixed dead link
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:38 +0200 |
haftmann |
fixed dead link
|
changeset |
files
|
| Tue, 27 Sep 2005 16:52:24 +0200 |
haftmann |
improved linkcheck
|
changeset |
files
|
| Tue, 27 Sep 2005 16:33:36 +0200 |
haftmann |
added simple linktester for isabelle website
|
changeset |
files
|
| Tue, 27 Sep 2005 16:28:11 +0200 |
wenzelm |
warn about Poly/ML segfault problem;
|
changeset |
files
|
| Tue, 27 Sep 2005 15:30:37 +0200 |
haftmann |
website preparation for Isabelle2005
|
changeset |
files
|
| Tue, 27 Sep 2005 14:41:41 +0200 |
obua |
corrected spelling bug
|
changeset |
files
|
| Tue, 27 Sep 2005 14:39:35 +0200 |
obua |
added defs disclaimer
|
changeset |
files
|
| Tue, 27 Sep 2005 12:16:06 +0200 |
berghofe |
nat_number_of is no longer declared as code lemma, since this turned
|
changeset |
files
|
| Tue, 27 Sep 2005 12:14:39 +0200 |
berghofe |
Inserted clause for nat in number_of_codegen again ("code unfold" turned
|
changeset |
files
|