| Wed, 31 Dec 2008 00:08:14 +0100 |
wenzelm |
use exists_subterm directly;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
use exists_subterm directly;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:08:11 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:01:51 +0100 |
wenzelm |
added old_term.ML;
|
changeset |
files
|
| Wed, 31 Dec 2008 00:01:07 +0100 |
wenzelm |
Some old-style term operations.
|
changeset |
files
|
| Tue, 30 Dec 2008 21:49:09 +0100 |
wenzelm |
freeze_thaw: canonical Term.add_XXX operations;
|
changeset |
files
|
| Tue, 30 Dec 2008 21:48:07 +0100 |
wenzelm |
varify: regular name context;
|
changeset |
files
|
| Tue, 30 Dec 2008 21:47:11 +0100 |
wenzelm |
canonical Term.add_var_names, Term.add_tvar_namesT;
|
changeset |
files
|
| Tue, 30 Dec 2008 21:46:48 +0100 |
wenzelm |
canonical Term.add_var_names;
|
changeset |
files
|
| Tue, 30 Dec 2008 21:46:14 +0100 |
wenzelm |
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
|
changeset |
files
|
| Tue, 30 Dec 2008 20:53:21 +0100 |
wenzelm |
removed unused head_name_of;
|
changeset |
files
|
| Tue, 30 Dec 2008 19:08:43 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 30 Dec 2008 19:07:42 +0100 |
wenzelm |
prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms;
|
changeset |
files
|
| Tue, 30 Dec 2008 16:50:46 +0100 |
ballarin |
New locales.
|
changeset |
files
|
| Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Tue, 30 Dec 2008 08:18:54 +0100 |
ballarin |
Temporarily avoid type errors in parse phase.
|
changeset |
files
|
| Tue, 23 Dec 2008 14:29:27 +0100 |
ballarin |
More liberal consistency check for defines elements.
|
changeset |
files
|
| Fri, 19 Dec 2008 16:39:23 +0100 |
ballarin |
All logics ported to new locales.
|
changeset |
files
|
| Fri, 19 Dec 2008 15:05:37 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Thu, 18 Dec 2008 11:16:48 +0100 |
Norbert Schirmer |
adapted statespace module to new locales;
|
changeset |
files
|
| Fri, 19 Dec 2008 14:31:17 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Fri, 19 Dec 2008 14:31:07 +0100 |
ballarin |
Intro_locales_tac knows about defines elements; more robust export morphism.
|
changeset |
files
|
| Fri, 19 Dec 2008 11:57:21 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Fri, 19 Dec 2008 11:09:31 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 19 Dec 2008 11:09:09 +0100 |
ballarin |
More porting to new locales
|
changeset |
files
|
| Thu, 18 Dec 2008 20:19:49 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Wed, 17 Dec 2008 17:53:56 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Wed, 17 Dec 2008 17:53:41 +0100 |
ballarin |
Prevent defines from being checked in interpretation.
|
changeset |
files
|
| Tue, 16 Dec 2008 21:11:39 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Tue, 16 Dec 2008 15:09:37 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Tue, 16 Dec 2008 15:09:12 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Mon, 15 Dec 2008 18:12:52 +0100 |
ballarin |
More porting to new locales.
|
changeset |
files
|
| Sun, 14 Dec 2008 18:45:51 +0100 |
ballarin |
Ported HOL and HOL-Library to new locales.
|
changeset |
files
|
| Sun, 14 Dec 2008 18:45:16 +0100 |
ballarin |
Fixed legacy locale keywords (went to ZF rather than default keywords file).
|
changeset |
files
|
| Sun, 14 Dec 2008 15:50:21 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 12 Dec 2008 20:10:22 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 12 Dec 2008 20:03:30 +0100 |
ballarin |
Porting to new locales.
|
changeset |
files
|
| Fri, 12 Dec 2008 17:00:42 +0100 |
ballarin |
Theory target distinguishes old and new locales.
|
changeset |
files
|
| Fri, 12 Dec 2008 15:02:15 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 12 Dec 2008 14:26:35 +0100 |
ballarin |
Ported to new locales.
|
changeset |
files
|
| Fri, 12 Dec 2008 14:23:49 +0100 |
ballarin |
Merged; updated interpretation command in isar_syn.ML.
|
changeset |
files
|
| Thu, 11 Dec 2008 18:34:05 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
changeset |
files
|
| Fri, 19 Dec 2008 11:07:36 +0100 |
ballarin |
Add inherited registrations.
|
changeset |
files
|
| Thu, 18 Dec 2008 19:52:11 +0100 |
ballarin |
Refactored: evaluate specification text only in locale declarations.
|
changeset |
files
|
| Wed, 17 Dec 2008 15:21:23 +0100 |
ballarin |
Transfer theorems in print_locale.
|
changeset |
files
|
| Wed, 17 Dec 2008 15:20:33 +0100 |
ballarin |
Attributes not applied in foundational version of fact.
|
changeset |
files
|
| Tue, 16 Dec 2008 20:18:46 +0100 |
ballarin |
Transfer morphism with theory closure.
|
changeset |
files
|
| Tue, 16 Dec 2008 15:08:08 +0100 |
ballarin |
Finer-grained activation so that facts from earlier elements are available.
|
changeset |
files
|
| Tue, 16 Dec 2008 14:29:05 +0100 |
ballarin |
Transfer theorems before activation.
|
changeset |
files
|
| Tue, 16 Dec 2008 12:08:10 +0100 |
ballarin |
Use correct mode when parsing elements and conclusion.
|
changeset |
files
|
| Sun, 14 Dec 2008 15:43:04 +0100 |
ballarin |
Strict prefixes in locales expressions.
|
changeset |
files
|
| Fri, 12 Dec 2008 19:58:26 +0100 |
ballarin |
Propagate theorems to registrations.
|
changeset |
files
|
| Fri, 12 Dec 2008 14:30:21 +0100 |
ballarin |
Automated merge with ssh://ballarin@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Fri, 12 Dec 2008 12:31:00 +0100 |
ballarin |
Equations in interpretation as goals.
|
changeset |
files
|
| Thu, 11 Dec 2008 17:56:34 +0100 |
ballarin |
Interpretation in theories: first version with equations.
|
changeset |
files
|
| Thu, 11 Dec 2008 17:55:51 +0100 |
ballarin |
Clarified comment.
|
changeset |
files
|
| Wed, 10 Dec 2008 17:19:25 +0100 |
ballarin |
Use prefix component of bindings for locale prefixes.
|
changeset |
files
|
| Wed, 10 Dec 2008 17:18:12 +0100 |
ballarin |
Missing dependency
|
changeset |
files
|
| Wed, 10 Dec 2008 16:30:33 +0100 |
ballarin |
Preserve idents (expression in sublocale).
|
changeset |
files
|
| Mon, 29 Dec 2008 22:43:41 +0100 |
wenzelm |
added POSITION_PROPERTIES;
|
changeset |
files
|
| Mon, 29 Dec 2008 22:36:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 29 Dec 2008 22:20:04 +0100 |
wenzelm |
override toString method;
|
changeset |
files
|
| Mon, 29 Dec 2008 20:06:31 +0100 |
wenzelm |
Swing utilities.
|
changeset |
files
|
| Mon, 29 Dec 2008 18:30:05 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 29 Dec 2008 18:27:33 +0100 |
wenzelm |
optional exception logging;
|
changeset |
files
|
| Mon, 29 Dec 2008 17:57:18 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 29 Dec 2008 17:56:37 +0100 |
haftmann |
pretty printer for bindings
|
changeset |
files
|
| Mon, 29 Dec 2008 14:08:08 +0100 |
haftmann |
adapted HOL source structure to distribution layout
|
changeset |
files
|
| Mon, 29 Dec 2008 16:45:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 29 Dec 2008 16:44:49 +0100 |
wenzelm |
more markup elements;
|
changeset |
files
|
| Mon, 29 Dec 2008 15:23:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 29 Dec 2008 15:16:25 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 29 Dec 2008 15:16:01 +0100 |
wenzelm |
explicit EventBus for results;
|
changeset |
files
|
| Mon, 29 Dec 2008 15:13:53 +0100 |
wenzelm |
added methods "+" and "-";
|
changeset |
files
|
| Mon, 29 Dec 2008 13:57:37 +0100 |
wenzelm |
Generic event bus.
|
changeset |
files
|
| Mon, 29 Dec 2008 13:23:53 +0100 |
haftmann |
eliminated fun/val confusion
|
changeset |
files
|
| Sun, 28 Dec 2008 14:41:47 -0800 |
huffman |
merged
|
changeset |
files
|
| Sun, 28 Dec 2008 14:40:43 -0800 |
huffman |
clean up proofs of lemma Maclaurin
|
changeset |
files
|
| Sun, 28 Dec 2008 23:20:57 +0100 |
wenzelm |
disabled old jedit plugin;
|
changeset |
files
|
| Sun, 28 Dec 2008 20:25:39 +0100 |
wenzelm |
more markup elements;
|
changeset |
files
|
| Sun, 28 Dec 2008 16:39:27 +0100 |
wenzelm |
more markup elements;
|
changeset |
files
|
| Sat, 27 Dec 2008 17:49:15 +0100 |
krauss |
removed duplicate sum_case used only by function package;
|
changeset |
files
|
| Sat, 27 Dec 2008 17:35:01 +0100 |
krauss |
tuned NEWS; CONTRIBUTORS
|
changeset |
files
|
| Sat, 27 Dec 2008 17:35:00 +0100 |
krauss |
renamed LexOrds.thy to Termination.thy; examples for sizechange method
|
changeset |
files
|
| Sat, 27 Dec 2008 17:09:27 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 27 Dec 2008 16:34:26 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 27 Dec 2008 16:33:50 +0100 |
wenzelm |
refined execute, which replaces exec/exec2;
|
changeset |
files
|
| Sat, 27 Dec 2008 16:33:19 +0100 |
wenzelm |
maintain initial process environment;
|
changeset |
files
|
| Sat, 27 Dec 2008 16:28:36 +0100 |
haftmann |
merged
|
changeset |
files
|
| Sat, 27 Dec 2008 16:28:13 +0100 |
haftmann |
tackling simultaneous val/fun bindings
|
changeset |
files
|
| Sat, 27 Dec 2008 14:57:30 +0100 |
wenzelm |
proper class IsabelleSystem -- no longer static;
|
changeset |
files
|
| Sat, 27 Dec 2008 11:54:08 +0100 |
wenzelm |
PATH: /opt/local/bin is back again (required for latex etc.);
|
changeset |
files
|
| Wed, 24 Dec 2008 13:39:20 -0800 |
huffman |
merged.
|
changeset |
files
|
| Wed, 24 Dec 2008 13:29:49 -0800 |
huffman |
clean up lemmas about ln
|
changeset |
files
|
| Wed, 24 Dec 2008 13:16:26 -0800 |
huffman |
clean up lemmas about exp
|
changeset |
files
|
| Wed, 24 Dec 2008 11:17:37 -0800 |
huffman |
more proofs about differentiable
|
changeset |
files
|
| Wed, 24 Dec 2008 09:26:18 -0800 |
huffman |
use less_iff_Suc_add instead of less_add_one
|
changeset |
files
|
| Wed, 24 Dec 2008 08:40:16 -0800 |
huffman |
rearranged subsections; cleaned up some proofs
|
changeset |
files
|
| Wed, 24 Dec 2008 08:16:45 -0800 |
huffman |
move theorems about limits from Transcendental.thy to Deriv.thy
|
changeset |
files
|
| Wed, 24 Dec 2008 08:06:27 -0800 |
huffman |
cleaned up some proofs; removed redundant simp rules
|
changeset |
files
|
| Tue, 23 Dec 2008 15:02:30 -0800 |
huffman |
move sin and cos to their own subsection
|
changeset |
files
|
| Tue, 23 Dec 2008 14:31:47 -0800 |
huffman |
clean up some proofs; remove unused lemmas
|
changeset |
files
|
| Tue, 23 Dec 2008 21:24:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 23 Dec 2008 21:18:26 +0100 |
wenzelm |
* Proofs of are run in parallel on multi-core systems;
|
changeset |
files
|
| Tue, 23 Dec 2008 21:03:47 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 23 Dec 2008 21:03:35 +0100 |
wenzelm |
updated thread-safe programming;
|
changeset |
files
|
| Tue, 23 Dec 2008 19:49:33 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 23 Dec 2008 19:49:21 +0100 |
wenzelm |
added float_token, and num_const, float_const;
|
changeset |
files
|
| Tue, 23 Dec 2008 19:27:42 +0100 |
wenzelm |
renamed terminal category "float" to "float_token", to avoid name
|
changeset |
files
|
| Tue, 23 Dec 2008 13:20:34 +0100 |
wenzelm |
manual file type setup using AppHack 1.1;
|
changeset |
files
|
| Tue, 23 Dec 2008 12:53:44 +0100 |
wenzelm |
target PWD;
|
changeset |
files
|
| Tue, 23 Dec 2008 11:04:07 +0100 |
wenzelm |
updated scala path;
|
changeset |
files
|
| Tue, 23 Dec 2008 00:56:03 +0100 |
wenzelm |
added platform_file;
|
changeset |
files
|
| Mon, 22 Dec 2008 19:57:49 +0100 |
wenzelm |
proper -X option;
|
changeset |
files
|
| Mon, 22 Dec 2008 16:57:11 +0100 |
wenzelm |
unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
|
changeset |
files
|
| Mon, 22 Dec 2008 14:40:27 +0100 |
wenzelm |
more sophisticated MacOS interface script (mostly for Carbon Emacs);
|
changeset |
files
|
| Sun, 21 Dec 2008 12:41:09 +0100 |
wenzelm |
updated web style for Mercurial 1.1.1;
|
changeset |
files
|
| Sun, 21 Dec 2008 12:30:00 +0100 |
wenzelm |
misc webstyle adaptions;
|
changeset |
files
|
| Sat, 20 Dec 2008 23:09:48 +0100 |
wenzelm |
updated web style for Mercurial 1.1;
|
changeset |
files
|
| Sat, 20 Dec 2008 11:55:34 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
| Sat, 20 Dec 2008 11:39:34 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 20 Dec 2008 11:39:27 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
| Fri, 19 Dec 2008 16:16:10 -0800 |
huffman |
merged.
|
changeset |
files
|
| Thu, 18 Dec 2008 11:00:13 -0800 |
huffman |
constdefs -> definition
|
changeset |
files
|
| Fri, 19 Dec 2008 20:37:29 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
| Thu, 18 Dec 2008 09:30:36 -0800 |
huffman |
merged.
|
changeset |
files
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
changeset |
files
|
| Wed, 17 Dec 2008 14:40:04 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 17 Dec 2008 14:39:38 +0100 |
wenzelm |
basic setup for MacOS application bundle;
|
changeset |
files
|
| Wed, 17 Dec 2008 12:10:40 +0100 |
haftmann |
GHC ext pragma in generated Haskell modules
|
changeset |
files
|
| Wed, 17 Dec 2008 12:10:39 +0100 |
haftmann |
dropped Ids
|
changeset |
files
|
| Wed, 17 Dec 2008 12:10:39 +0100 |
haftmann |
temporary adaption to new locale code
|
changeset |
files
|
| Wed, 17 Dec 2008 12:10:38 +0100 |
haftmann |
restructured; circumvent sort problem
|
changeset |
files
|
| Tue, 16 Dec 2008 21:18:53 -0800 |
huffman |
merged.
|
changeset |
files
|
| Tue, 16 Dec 2008 09:44:59 -0800 |
huffman |
new theory Dsum: cpo of disjoint sum
|
changeset |
files
|
| Tue, 16 Dec 2008 09:10:09 -0800 |
huffman |
scale dependency graph in document
|
changeset |
files
|
| Tue, 16 Dec 2008 20:32:41 +0000 |
Christian Urban |
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
|
changeset |
files
|
| Tue, 16 Dec 2008 19:24:55 +0100 |
wenzelm |
proper document antiquotations;
|
changeset |
files
|
| Tue, 16 Dec 2008 18:04:31 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 16 Dec 2008 08:46:07 +0100 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
changeset |
files
|
| Tue, 16 Dec 2008 18:04:16 +0100 |
wenzelm |
future proofs: Future.fork_pri 1 minimizes queue length and pending promises
|
changeset |
files
|
| Tue, 16 Dec 2008 16:25:20 +0100 |
wenzelm |
renamed structure TaskQueue to Task_Queue;
|
changeset |
files
|
| Tue, 16 Dec 2008 16:25:19 +0100 |
wenzelm |
Future.fork_pri;
|
changeset |
files
|
| Tue, 16 Dec 2008 16:25:19 +0100 |
wenzelm |
renamed structure TaskQueue to Task_Queue;
|
changeset |
files
|
| Tue, 16 Dec 2008 16:25:19 +0100 |
wenzelm |
renamed structure TaskQueue to Task_Queue;
|
changeset |
files
|
| Tue, 16 Dec 2008 16:25:18 +0100 |
wenzelm |
renamed structure TaskQueue to Task_Queue;
|
changeset |
files
|
| Tue, 16 Dec 2008 12:13:53 +0100 |
wenzelm |
removed old scheduler;
|
changeset |
files
|
| Tue, 16 Dec 2008 00:19:47 +0100 |
wenzelm |
tuned enqueue: plain add_edge, acyclic not required here;
|
changeset |
files
|
| Mon, 15 Dec 2008 22:07:30 +0100 |
wenzelm |
tuned messages;
|
changeset |
files
|
| Mon, 15 Dec 2008 21:55:21 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Mon, 15 Dec 2008 21:54:37 +0100 |
wenzelm |
repaired railroad accident;
|
changeset |
files
|
| Mon, 15 Dec 2008 21:41:21 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Mon, 15 Dec 2008 21:41:00 +0100 |
wenzelm |
added 'atp_messages' command, which displays recent messages synchronously;
|
changeset |
files
|
| Mon, 15 Dec 2008 10:19:02 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 15 Dec 2008 10:16:38 +0100 |
nipkow |
flipped fold implementation
|
changeset |
files
|
| Thu, 11 Dec 2008 08:59:03 +0100 |
nipkow |
merged
|
changeset |
files
|
| Thu, 11 Dec 2008 08:56:02 +0100 |
nipkow |
codegen
|
changeset |
files
|
| Thu, 11 Dec 2008 08:53:53 +0100 |
nipkow |
code for {x:A. P(x)} and for fold
|
changeset |
files
|
| Thu, 11 Dec 2008 08:52:50 +0100 |
nipkow |
Testfile for Stefan's code generator
|
changeset |
files
|
| Mon, 15 Dec 2008 09:58:45 +0100 |
haftmann |
moved value.ML to src/Tools
|
changeset |
files
|
| Mon, 15 Dec 2008 09:58:44 +0100 |
haftmann |
\underscoreoff is now default
|
changeset |
files
|
| Mon, 15 Dec 2008 07:41:07 +0000 |
Christian Urban |
tuned some proofs
|
changeset |
files
|
| Sat, 13 Dec 2008 17:46:13 +0100 |
wenzelm |
removed Ids;
|
changeset |
files
|
| Sat, 13 Dec 2008 17:13:09 +0100 |
berghofe |
merged
|
changeset |
files
|
| Sat, 13 Dec 2008 16:59:33 +0100 |
berghofe |
merged
|
changeset |
files
|
| Sat, 13 Dec 2008 16:29:33 +0100 |
berghofe |
merged
|
changeset |
files
|
| Sat, 13 Dec 2008 16:26:06 +0100 |
berghofe |
Unified syntax of nominal_primrec with the one used by fun(ction) and new
|
changeset |
files
|
| Sat, 13 Dec 2008 13:24:45 +0100 |
berghofe |
Modified nominal_primrec to make it work with local theories, unified syntax
|
changeset |
files
|
| Sat, 13 Dec 2008 15:35:29 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 13 Dec 2008 15:35:18 +0100 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 13 Dec 2008 15:07:56 +0100 |
wenzelm |
tuned ML_OPTIONS for improved multicore performance;
|
changeset |
files
|
| Sat, 13 Dec 2008 15:06:24 +0100 |
wenzelm |
refined identity and ancestry: explicit draft flat, ids are unnamed, name consistency is checked for ancestry;
|
changeset |
files
|
| Sat, 13 Dec 2008 15:00:40 +0100 |
wenzelm |
requires: check ancestors directly;
|
changeset |
files
|
| Sat, 13 Dec 2008 15:00:39 +0100 |
wenzelm |
Context.display_names;
|
changeset |
files
|
| Fri, 12 Dec 2008 22:13:13 +0100 |
wenzelm |
global_qed: refrain from ProofContext.auto_bind_facts, to avoid
|
changeset |
files
|
| Sat, 13 Dec 2008 15:33:13 +0100 |
wenzelm |
usage: echo ML settings as well;
|
changeset |
files
|
| Fri, 12 Dec 2008 12:14:02 +0100 |
wenzelm |
future proofs: more robust check via Future.enabled;
|
changeset |
files
|
| Thu, 11 Dec 2008 22:53:50 +0100 |
wenzelm |
removed former Isabelle font (cf. IsabelleItalic);
|
changeset |
files
|
| Thu, 11 Dec 2008 22:38:00 +0100 |
wenzelm |
incorporated isabelle-fonts side-branch (forced merge);
|
changeset |
files
|
| Sat, 06 Sep 2008 21:55:43 +0200 |
wenzelm |
replaced single quote by mathematical prime;
|
changeset |
files
|
| Sun, 24 Aug 2008 14:59:45 +0200 |
wenzelm |
generated file;
|
changeset |
files
|
| Sun, 24 Aug 2008 14:59:34 +0200 |
wenzelm |
bold version: math glyphs from plain IsabelleMono;
|
changeset |
files
|
| Sun, 24 Aug 2008 14:43:59 +0200 |
wenzelm |
fixed rangle;
|
changeset |
files
|
| Sun, 24 Aug 2008 14:33:26 +0200 |
wenzelm |
use dash from text font, not math;
|
changeset |
files
|
| Sun, 24 Aug 2008 14:19:34 +0200 |
wenzelm |
added glyphs for \<A> (cal), \<a> (rm), \<AA> (\frak), \<aa> (frak);
|
changeset |
files
|
| Fri, 22 Aug 2008 18:38:00 +0200 |
wenzelm |
generated ttf;
|
changeset |
files
|
| Fri, 22 Aug 2008 18:35:15 +0200 |
wenzelm |
renamed to IsabelleMono;
|
changeset |
files
|
| Fri, 22 Aug 2008 18:31:02 +0200 |
wenzelm |
added README with original licenses;
|
changeset |
files
|
| Fri, 22 Aug 2008 17:54:40 +0200 |
wenzelm |
renamed Isabelle to IsabelleItalic;
|
changeset |
files
|
| Fri, 22 Aug 2008 17:53:15 +0200 |
wenzelm |
fixed rangle glyph;
|
changeset |
files
|
| Fri, 22 Aug 2008 17:49:42 +0200 |
wenzelm |
the other way round: import Isabelle font (222%) into Bitstream Vera Mono -- achieves better quality;
|
changeset |
files
|
| Fri, 22 Aug 2008 17:06:19 +0200 |
wenzelm |
Isabelle font with digits and letters from Bitstream Vera Mono (scaled 45%);
|
changeset |
files
|
| Fri, 22 Aug 2008 17:05:46 +0200 |
wenzelm |
Isabelle font, based on TeX glyhps;
|
changeset |
files
|
| Thu, 11 Dec 2008 22:25:39 +0100 |
wenzelm |
enable future_scheduler by default;
|
changeset |
files
|
| Thu, 11 Dec 2008 21:31:42 +0100 |
wenzelm |
ISABELLE_USEDIR_OPTIONS: -M max is default;
|
changeset |
files
|
| Thu, 11 Dec 2008 20:31:45 +0100 |
wenzelm |
unified ids for ancestors and checkpoints, removed obsolete history of checkpoints;
|
changeset |
files
|
| Thu, 11 Dec 2008 20:17:57 +0100 |
wenzelm |
removed spurious exception_trace;
|
changeset |
files
|
| Thu, 11 Dec 2008 17:32:37 +0100 |
wenzelm |
print_theorems: more robust difference, even after finished proof;
|
changeset |
files
|
| Thu, 11 Dec 2008 17:31:23 +0100 |
wenzelm |
export context_node;
|
changeset |
files
|
| Thu, 11 Dec 2008 17:04:46 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Dec 2008 22:55:15 +0100 |
wenzelm |
more antiquotations;
|
changeset |
files
|
| Thu, 11 Dec 2008 16:50:18 +0100 |
wenzelm |
pcpodef package: state two goals, instead of encoded conjunction;
|
changeset |
files
|
| Thu, 11 Dec 2008 16:30:35 +0100 |
wenzelm |
recovered goal_pat;
|
changeset |
files
|
| Thu, 11 Dec 2008 16:09:12 +0100 |
wenzelm |
inhabitance goal is now stated in original form and result contracted --
|
changeset |
files
|
| Thu, 11 Dec 2008 12:02:48 +0100 |
wenzelm |
tuned signature: pcpodef_proof, pcpodef_proof_cmd etc.;
|
changeset |
files
|
| Thu, 11 Dec 2008 11:55:46 +0100 |
wenzelm |
add_typedef: unfold set_def in tactical proof as well;
|
changeset |
files
|
| Thu, 11 Dec 2008 10:41:53 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 11 Dec 2008 10:41:37 +0100 |
wenzelm |
Theory.checkpoint before commencing proof;
|
changeset |
files
|
| Thu, 11 Dec 2008 00:42:52 +0100 |
wenzelm |
misc tuning and modernisation;
|
changeset |
files
|
| Wed, 10 Dec 2008 22:05:58 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 08 Dec 2008 08:56:30 +0100 |
krauss |
logically separate typedef axiomatization from constant definition
|
changeset |
files
|
| Mon, 08 Dec 2008 08:36:16 +0100 |
krauss |
add def before setting up goal
|
changeset |
files
|
| Sun, 07 Dec 2008 20:41:23 +0100 |
krauss |
killed dead code
|
changeset |
files
|
| Thu, 11 Dec 2008 09:02:22 +0100 |
krauss |
constrain type inference to sort "type"
|
changeset |
files
|
| Wed, 10 Dec 2008 17:22:34 -0800 |
huffman |
merged.
|
changeset |
files
|
| Wed, 10 Dec 2008 17:15:26 -0800 |
huffman |
cleaned up some proofs in Cfun.thy
|
changeset |
files
|
| Wed, 10 Dec 2008 15:31:55 -0800 |
huffman |
implement cont_proc theorem cache using theory data
|
changeset |
files
|
| Wed, 10 Dec 2008 13:44:09 -0800 |
huffman |
use ML antiquotations
|
changeset |
files
|
| Wed, 10 Dec 2008 12:31:35 -0800 |
huffman |
clean up diff_bin_simps
|
changeset |
files
|
| Wed, 10 Dec 2008 07:52:54 -0800 |
huffman |
move nat_{div,mod}_distrib from NatBin to IntDiv, simplified proofs
|
changeset |
files
|
| Wed, 10 Dec 2008 23:54:03 +0100 |
wenzelm |
fixed import: requires ContNotDenum;
|
changeset |
files
|
| Wed, 10 Dec 2008 23:13:21 +0100 |
wenzelm |
fixed import: requires ContNotDenum;
|
changeset |
files
|
| Wed, 10 Dec 2008 22:46:42 +0100 |
wenzelm |
requires RComplete;
|
changeset |
files
|
| Wed, 10 Dec 2008 06:34:10 -0800 |
huffman |
merged.
|
changeset |
files
|
| Tue, 09 Dec 2008 22:13:16 -0800 |
huffman |
move all neg-related lemmas to NatBin; make type of neg specific to int
|
changeset |
files
|
| Tue, 09 Dec 2008 20:36:20 -0800 |
huffman |
separate neg_simps from rel_simps
|
changeset |
files
|
| Tue, 09 Dec 2008 20:35:31 -0800 |
huffman |
use {less,le}_number_of in integer simprocs
|
changeset |
files
|
| Tue, 09 Dec 2008 16:26:47 -0800 |
huffman |
use lemma lists defined in Int.thy
|
changeset |
files
|
| Wed, 10 Dec 2008 14:45:15 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Wed, 10 Dec 2008 14:21:42 +0100 |
ballarin |
Satisfy a_axioms.
|
changeset |
files
|
| Wed, 10 Dec 2008 10:12:44 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Wed, 10 Dec 2008 10:11:18 +0100 |
ballarin |
Enable keyword 'structure' in for clause of locale expression.
|
changeset |
files
|
| Tue, 09 Dec 2008 22:00:39 +0100 |
ballarin |
Correct order of defines in specification.
|
changeset |
files
|
| Tue, 09 Dec 2008 21:27:00 +0100 |
ballarin |
Pass on defines in inheritance; reject illicit defines created by instantiation.
|
changeset |
files
|
| Tue, 09 Dec 2008 15:34:49 +0100 |
ballarin |
Order of implicit parameters in locale expression.
|
changeset |
files
|
| Tue, 09 Dec 2008 13:11:42 +0100 |
ballarin |
NewLocale.intro_locales_tac added to Class.default_intro_tac.
|
changeset |
files
|
| Tue, 09 Dec 2008 11:30:24 +0100 |
ballarin |
When adding locales, delay notes until local theory is built.
|
changeset |
files
|
| Wed, 10 Dec 2008 10:28:16 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 10 Dec 2008 10:23:47 +0100 |
nipkow |
moved ContNotDenum into Library
|
changeset |
files
|
| Tue, 09 Dec 2008 15:31:38 -0800 |
huffman |
move lemmas from Numeral_Type.thy to other theories
|
changeset |
files
|
| Tue, 09 Dec 2008 12:53:25 -0800 |
huffman |
instantiation option :: (enum) enum
|
changeset |
files
|
| Tue, 09 Dec 2008 11:49:12 -0800 |
huffman |
instance inat :: semiring_char_0
|
changeset |
files
|
| Mon, 08 Dec 2008 21:33:50 +0100 |
ballarin |
Default names for definitions.
|
changeset |
files
|
| Mon, 08 Dec 2008 18:44:24 +0100 |
ballarin |
Proper shape of assumptions generated from Defines elements.
|
changeset |
files
|
| Mon, 08 Dec 2008 14:22:42 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Mon, 08 Dec 2008 14:18:29 +0100 |
ballarin |
Explicitly close up defines.
|
changeset |
files
|
| Fri, 05 Dec 2008 16:41:36 +0100 |
ballarin |
Interpretation in proof contexts.
|
changeset |
files
|
| Mon, 08 Dec 2008 10:27:40 +0100 |
haftmann |
tuned LaTeX files
|
changeset |
files
|
| Mon, 08 Dec 2008 10:14:50 +0100 |
haftmann |
tuned LaTeX files
|
changeset |
files
|
| Sat, 06 Dec 2008 23:19:44 -0800 |
huffman |
merged.
|
changeset |
files
|
| Sat, 06 Dec 2008 20:26:51 -0800 |
huffman |
multiplication for type inat
|
changeset |
files
|
| Sat, 06 Dec 2008 20:25:31 -0800 |
huffman |
fix proofs
|
changeset |
files
|
| Sat, 06 Dec 2008 19:39:53 -0800 |
huffman |
change lemmas to avoid using neg
|
changeset |
files
|
| Fri, 05 Dec 2008 17:35:22 -0800 |
huffman |
simplify less_nat_number_of
|
changeset |
files
|
| Fri, 05 Dec 2008 17:26:16 -0800 |
huffman |
add lemma le_nat_number_of
|
changeset |
files
|
| Sat, 06 Dec 2008 12:18:05 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sat, 06 Dec 2008 08:57:39 +0100 |
haftmann |
adapted to changes in binding module
|
changeset |
files
|
| Sat, 06 Dec 2008 08:45:38 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
changeset |
files
|
| Fri, 05 Dec 2008 18:42:39 +0100 |
haftmann |
corrected theory path
|
changeset |
files
|
| Fri, 05 Dec 2008 18:42:37 +0100 |
haftmann |
removed Table.extend, NameSpace.extend_table
|
changeset |
files
|
| Sat, 06 Dec 2008 00:09:01 +0100 |
wenzelm |
renamed force_proof to join_proof;
|
changeset |
files
|
| Sat, 06 Dec 2008 00:08:32 +0100 |
wenzelm |
renamed force_proofs to join_proofs;
|
changeset |
files
|
| Sat, 06 Dec 2008 00:08:07 +0100 |
wenzelm |
finish_thy: to not collapse checkpoints -- allows future proofs to be deferred indefinitely (performance tradeoff: 5-15% slowdown in sequential batch jobs);
|
changeset |
files
|
| Sat, 06 Dec 2008 00:04:44 +0100 |
wenzelm |
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
|
changeset |
files
|
| Sat, 06 Dec 2008 00:03:28 +0100 |
wenzelm |
excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
|
changeset |
files
|
| Sat, 06 Dec 2008 00:02:11 +0100 |
wenzelm |
added new_task;
|
changeset |
files
|
| Sat, 06 Dec 2008 00:01:57 +0100 |
wenzelm |
added constant value;
|
changeset |
files
|
| Fri, 05 Dec 2008 20:38:40 +0100 |
wenzelm |
refined type deriv: replaced all_promises by max_promise (dependency limit) and open_promises (potentially unfinished/failed promises);
|
changeset |
files
|
| Fri, 05 Dec 2008 18:15:52 +0100 |
wenzelm |
uniform treatment of ISABELLE_HOME/contrib vs. ISABELLE_HOME/..;
|
changeset |
files
|
| Fri, 05 Dec 2008 11:42:27 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Fri, 05 Dec 2008 11:26:07 +0100 |
ballarin |
Interpretation in theories including interaction with subclass relation.
|
changeset |
files
|
| Fri, 05 Dec 2008 08:05:14 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
changeset |
files
|
| Thu, 04 Dec 2008 18:37:46 -0800 |
huffman |
fix proofs
|
changeset |
files
|
| Thu, 04 Dec 2008 16:44:37 -0800 |
huffman |
merged.
|
changeset |
files
|
| Thu, 04 Dec 2008 16:28:09 -0800 |
huffman |
revert to using eq_number_of_eq for simplification (Groebner_Examples.thy was broken)
|
changeset |
files
|
| Thu, 04 Dec 2008 16:05:45 -0800 |
huffman |
remove duplicated lemmas
|
changeset |
files
|
| Thu, 04 Dec 2008 13:30:09 -0800 |
huffman |
include iszero_simps in lemmas comp_arith
|
changeset |
files
|
| Thu, 04 Dec 2008 12:32:38 -0800 |
huffman |
add named lemma lists: neg_simps and iszero_simps
|
changeset |
files
|
| Thu, 04 Dec 2008 11:14:24 -0800 |
huffman |
change arith_special simps to avoid using neg
|
changeset |
files
|
| Fri, 05 Dec 2008 11:35:07 +1100 |
kleing |
merged
|
changeset |
files
|
| Fri, 05 Dec 2008 11:33:03 +1100 |
kleing |
run test for sunbroy2 on /tmp,
|
changeset |
files
|
| Fri, 05 Dec 2008 00:23:37 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 04 Dec 2008 23:46:20 +0100 |
wenzelm |
refined Future.fork interfaces, no longer export Future.future;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:46:20 +0100 |
wenzelm |
fork/map: no inheritance of group (structure is nested, not parallel);
|
changeset |
files
|
| Thu, 04 Dec 2008 23:02:56 +0100 |
wenzelm |
future proofs: pass actual futures to facilitate composite computations;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:02:52 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:02:46 +0100 |
wenzelm |
future_scheduler: no global task group, exceptions via collective join;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:01:11 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:01:03 +0100 |
wenzelm |
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:00:58 +0100 |
wenzelm |
future proofs: pass actual futures to facilitate composite computations;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:00:27 +0100 |
wenzelm |
renamed type Future.T to future;
|
changeset |
files
|
| Thu, 04 Dec 2008 23:00:21 +0100 |
wenzelm |
renamed type Lazy.T to lazy;
|
changeset |
files
|
| Thu, 04 Dec 2008 09:12:41 -0800 |
huffman |
merged.
|
changeset |
files
|
| Thu, 04 Dec 2008 08:47:45 -0800 |
huffman |
change more lemmas to avoid using iszero
|
changeset |
files
|
| Wed, 03 Dec 2008 22:16:20 -0800 |
huffman |
change some lemmas to avoid using iszero
|
changeset |
files
|
| Wed, 03 Dec 2008 21:50:36 -0800 |
huffman |
enable eq_bin_simps for simplifying equalities on numerals
|
changeset |
files
|
| Thu, 04 Dec 2008 14:44:07 +0100 |
haftmann |
merged
|
changeset |
files
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
changeset |
files
|
| Thu, 04 Dec 2008 14:17:36 +0100 |
nipkow |
NEWS
|
changeset |
files
|
| Wed, 03 Dec 2008 21:00:39 -0800 |
huffman |
fix proofs related to simplification of inequalities on numerals
|
changeset |
files
|
| Wed, 03 Dec 2008 20:45:42 -0800 |
huffman |
enable le_bin_simps and less_bin_simps for simplifying inequalities on numerals
|
changeset |
files
|
| Wed, 03 Dec 2008 20:24:17 -0800 |
huffman |
simplify proof of less_nat_number_of
|
changeset |
files
|
| Wed, 03 Dec 2008 15:04:37 -0800 |
huffman |
merged.
|
changeset |
files
|
| Wed, 03 Dec 2008 15:00:50 -0800 |
huffman |
fixed proofs due to changes in Int.thy
|
changeset |
files
|
| Wed, 03 Dec 2008 14:23:03 -0800 |
huffman |
cleaned up subsection headings;
|
changeset |
files
|
| Wed, 03 Dec 2008 21:22:38 +0100 |
wenzelm |
sources are not executable;
|
changeset |
files
|
| Wed, 03 Dec 2008 21:15:46 +0100 |
wenzelm |
eliminated traces of old Distribution directory;
|
changeset |
files
|
| Wed, 03 Dec 2008 21:02:20 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 03 Dec 2008 21:02:12 +0100 |
wenzelm |
remove *.lof as well;
|
changeset |
files
|
| Wed, 03 Dec 2008 15:59:56 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
changeset |
files
|
| Wed, 03 Dec 2008 15:27:41 +0100 |
ballarin |
Sublocale: removed public after_qed; identifiers private to NewLocale.
|
changeset |
files
|
| Wed, 03 Dec 2008 15:26:46 +0100 |
ballarin |
Made global_note_qualified public.
|
changeset |
files
|
| Wed, 03 Dec 2008 14:02:24 +0000 |
webertj |
more examples
|
changeset |
files
|
| Wed, 03 Dec 2008 09:53:58 +0100 |
haftmann |
fixed typo
|
changeset |
files
|
| Wed, 03 Dec 2008 09:51:35 +0100 |
haftmann |
unfold_locales is default method - no need for explicit references
|
changeset |
files
|
| Tue, 02 Dec 2008 17:50:39 +0100 |
wenzelm |
Automated merge with file:///mnt/home/isabelle-repository/repos/isabelle
|
changeset |
files
|
| Tue, 02 Dec 2008 14:29:12 +0100 |
berghofe |
Corrected imports.
|
changeset |
files
|
| Mon, 01 Dec 2008 15:36:48 -0800 |
huffman |
clean up imports related to ContNotDenum
|
changeset |
files
|
| Mon, 01 Dec 2008 22:00:38 +0100 |
wenzelm |
ignore aux stuff in doc-src;
|
changeset |
files
|
| Mon, 01 Dec 2008 19:42:26 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 01 Dec 2008 19:41:16 +0100 |
haftmann |
new Binding module
|
changeset |
files
|
| Mon, 01 Dec 2008 16:02:57 +0100 |
haftmann |
Locale.*note* with conventional argument type
|
changeset |
files
|
| Mon, 01 Dec 2008 14:56:08 +0100 |
haftmann |
added code equation for subset
|
changeset |
files
|
| Mon, 01 Dec 2008 17:38:17 +0100 |
ballarin |
Merged again.
|
changeset |
files
|
| Mon, 01 Dec 2008 17:37:02 +0100 |
ballarin |
Merged.
|
changeset |
files
|
| Mon, 01 Dec 2008 16:59:31 +0100 |
ballarin |
No resolution of patterns within context statements.
|
changeset |
files
|
| Tue, 02 Dec 2008 17:50:25 +0100 |
wenzelm |
removed CVS Id;
|
changeset |
files
|
| Mon, 01 Dec 2008 17:48:12 +0100 |
wenzelm |
proper check of ISABELLE_TOOLS directories;
|
changeset |
files
|
| Mon, 01 Dec 2008 17:32:40 +0100 |
wenzelm |
removed obsolete tags (leftover from old CVS branches);
|
changeset |
files
|
| Mon, 01 Dec 2008 17:07:06 +0100 |
wenzelm |
makedist -- make Isabelle source distribution (Mercurial version);
|
changeset |
files
|
| Mon, 01 Dec 2008 15:22:17 +0100 |
wenzelm |
renamed makedist_mercurial to makedist, deleting the old version;
|
changeset |
files
|
| Mon, 01 Dec 2008 14:46:27 +0100 |
wenzelm |
updated to python2.5;
|
changeset |
files
|
| Mon, 01 Dec 2008 14:42:24 +0100 |
wenzelm |
convert to isabelle-cvs, the old version;
|
changeset |
files
|
| Mon, 01 Dec 2008 14:41:13 +0100 |
wenzelm |
adapted description: old CVS;
|
changeset |
files
|
| Mon, 01 Dec 2008 13:43:32 +0100 |
ballarin |
Methods intro_locales and unfold_locales apply to both old and new locales.
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:04 +0100 |
haftmann |
code_include with attach
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:03 +0100 |
haftmann |
experimental implementation of a well-sorting algorithm
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:02 +0100 |
haftmann |
code_funcgr interface includes also sort algebra
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:01 +0100 |
haftmann |
exported get_accesses (for diagnostic purpose)
|
changeset |
files
|
| Mon, 01 Dec 2008 12:17:00 +0100 |
haftmann |
more means for algebra projection
|
changeset |
files
|
| Mon, 01 Dec 2008 12:16:59 +0100 |
haftmann |
consider TeX spacing conventions for punctuation marks
|
changeset |
files
|
| Sun, 30 Nov 2008 18:10:00 +0100 |
huffman |
fix typed print translation for card UNIV
|
changeset |
files
|
| Sun, 30 Nov 2008 16:00:16 +0100 |
wenzelm |
removed obsolete CVS instructions;
|
changeset |
files
|
| Sun, 30 Nov 2008 15:03:47 +0100 |
wenzelm |
fixed spelling;
|
changeset |
files
|
| Sun, 30 Nov 2008 14:43:29 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 30 Nov 2008 14:03:46 +0100 |
wenzelm |
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
|
changeset |
files
|
| Sun, 30 Nov 2008 14:03:45 +0100 |
wenzelm |
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
|
changeset |
files
|
| Sun, 30 Nov 2008 12:58:20 +0100 |
wenzelm |
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
|
changeset |
files
|
| Sun, 30 Nov 2008 12:25:54 +0100 |
wenzelm |
misc tuning and clarification;
|
changeset |
files
|
| Sat, 29 Nov 2008 19:21:32 +0100 |
wenzelm |
remove repository-only files;
|
changeset |
files
|
| Sat, 29 Nov 2008 19:20:12 +0100 |
wenzelm |
more .hgignore entries;
|
changeset |
files
|
| Sat, 29 Nov 2008 19:01:28 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 29 Nov 2008 18:26:53 +0100 |
wenzelm |
basic setup of .hgignore;
|
changeset |
files
|
| Sat, 29 Nov 2008 18:19:59 +0100 |
wenzelm |
further notes;
|
changeset |
files
|
| Sat, 29 Nov 2008 17:09:28 +0100 |
wenzelm |
Important notes on Mercurial repository access for Isabelle.
|
changeset |
files
|
| Sat, 29 Nov 2008 13:39:45 +0100 |
nipkow |
Floats for Real.
|
changeset |
files
|
| Sat, 29 Nov 2008 13:39:23 +0100 |
nipkow |
new file float_syntax.ML
|
changeset |
files
|
| Sat, 29 Nov 2008 13:37:13 +0100 |
nipkow |
New lexical item "float".
|
changeset |
files
|
| Fri, 28 Nov 2008 17:43:06 +0100 |
ballarin |
Intro_locales_tac to simplify goals involving locale predicates.
|
changeset |
files
|
| Fri, 28 Nov 2008 12:26:14 +0100 |
ballarin |
Ahere to modern naming conventions; proper treatment of internal vs external names.
|
changeset |
files
|
| Fri, 28 Nov 2008 11:55:46 +0100 |
kleing |
added Tim's find_theorems performance patch
|
changeset |
files
|
| Fri, 28 Nov 2008 11:37:20 +0100 |
kleing |
FindTheorems performance improvements (from Timothy Bourke)
|
changeset |
files
|
| Fri, 28 Nov 2008 11:14:13 +0100 |
ballarin |
Perform higher-order pattern matching during round-up.
|
changeset |
files
|
| Thu, 27 Nov 2008 21:25:34 +0100 |
ballarin |
Proper treatment of expressions with free arguments.
|
changeset |
files
|
| Thu, 27 Nov 2008 21:25:16 +0100 |
ballarin |
Roundup bound.
|
changeset |
files
|
| Thu, 27 Nov 2008 10:30:42 +0100 |
ballarin |
Tests for sublocale command.
|
changeset |
files
|
| Thu, 27 Nov 2008 10:29:07 +0100 |
ballarin |
Sublocale command.
|
changeset |
files
|
| Thu, 27 Nov 2008 10:28:27 +0100 |
ballarin |
Command to add dependencies, fixed processing of dependencies.
|
changeset |
files
|
| Thu, 27 Nov 2008 10:26:00 +0100 |
ballarin |
Fixed strange indentation.
|
changeset |
files
|
| Tue, 25 Nov 2008 23:29:26 +0100 |
huffman |
add Algebraic and Universal to imports
|
changeset |
files
|
| Tue, 25 Nov 2008 23:29:01 +0100 |
huffman |
separate run and cases combinators
|
changeset |
files
|
| Tue, 25 Nov 2008 23:28:06 +0100 |
huffman |
renamed lemma compact_minimal to compact_bot_minimal;
|
changeset |
files
|
| Tue, 25 Nov 2008 23:26:44 +0100 |
huffman |
renamed lemma compact_minimal to compact_bot_minimal
|
changeset |
files
|
| Tue, 25 Nov 2008 18:07:33 +0100 |
ballarin |
Use standard export function.
|
changeset |
files
|
| Tue, 25 Nov 2008 18:07:01 +0100 |
ballarin |
Expression types cleaned up.
|
changeset |
files
|
| Tue, 25 Nov 2008 18:06:49 +0100 |
ballarin |
Test for term patterns added.
|
changeset |
files
|
| Tue, 25 Nov 2008 18:06:21 +0100 |
ballarin |
Expression types cleaned up, proper treatment of term patterns.
|
changeset |
files
|
| Mon, 24 Nov 2008 21:09:31 +0100 |
krauss |
check for more common errors first
|
changeset |
files
|
| Mon, 24 Nov 2008 21:00:03 +0100 |
krauss |
improved error msg; tuned
|
changeset |
files
|
| Mon, 24 Nov 2008 20:12:23 +0100 |
krauss |
removed "log" again, as IntInf.log2 already exists.
|
changeset |
files
|
| Mon, 24 Nov 2008 18:05:20 +0100 |
ballarin |
Some regression tests for theorem statements.
|
changeset |
files
|
| Mon, 24 Nov 2008 18:04:21 +0100 |
ballarin |
Enable switching to new locales during session.
|
changeset |
files
|
| Mon, 24 Nov 2008 18:03:48 +0100 |
ballarin |
Read/cert_statement for theorem statements.
|
changeset |
files
|
| Mon, 24 Nov 2008 18:02:52 +0100 |
ballarin |
Generalised activation code.
|
changeset |
files
|
| Mon, 24 Nov 2008 14:23:04 +0100 |
ballarin |
More ramifications of removal of 'includes' element.
|
changeset |
files
|
| Sun, 23 Nov 2008 18:37:56 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 23 Nov 2008 17:27:15 +0100 |
wenzelm |
eliminated finish_proof, keep pre/post normalization of results separate;
|
changeset |
files
|
| Sun, 23 Nov 2008 17:25:56 +0100 |
wenzelm |
future: norm_proof after make_result reduces memory requirements but increases runtime (factor 1.5 for both for HOL with proof terms);
|
changeset |
files
|
| Fri, 21 Nov 2008 18:02:19 +0100 |
ballarin |
Regression tests for new locale implementation.
|
changeset |
files
|
| Fri, 21 Nov 2008 18:01:39 +0100 |
ballarin |
add_locale functional.
|
changeset |
files
|
| Fri, 21 Nov 2008 15:54:53 +0100 |
paulson |
Added a line that was missing from the definition
|
changeset |
files
|
| Fri, 21 Nov 2008 14:21:42 +0100 |
krauss |
added binary logarithm
|
changeset |
files
|
| Fri, 21 Nov 2008 13:17:43 +0100 |
paulson |
Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.
|
changeset |
files
|
| Fri, 21 Nov 2008 07:34:36 +0100 |
haftmann |
Name.binding
|
changeset |
files
|
| Thu, 20 Nov 2008 22:39:12 +0100 |
nipkow |
added optimizer
|
changeset |
files
|
| Thu, 20 Nov 2008 19:43:34 +0100 |
wenzelm |
reactivated some dead theories (based on hints by Mark Hillebrand);
|
changeset |
files
|
| Thu, 20 Nov 2008 19:06:05 +0100 |
haftmann |
Locale.local_note_qualified
|
changeset |
files
|
| Thu, 20 Nov 2008 19:06:03 +0100 |
haftmann |
fact table now using name bindings
|
changeset |
files
|
| Thu, 20 Nov 2008 19:06:02 +0100 |
haftmann |
dropped legacy naming code
|
changeset |
files
|
| Thu, 20 Nov 2008 14:55:28 +0100 |
haftmann |
tuned name bindings
|
changeset |
files
|
| Thu, 20 Nov 2008 14:55:25 +0100 |
haftmann |
using name bindings
|
changeset |
files
|
| Thu, 20 Nov 2008 14:51:40 +0100 |
haftmann |
name spaces and name bindings
|
changeset |
files
|
| Thu, 20 Nov 2008 10:29:35 +0100 |
ballarin |
Deleted debug message (PolyML).
|
changeset |
files
|
| Thu, 20 Nov 2008 00:03:55 +0100 |
wenzelm |
removed traces of former 'includes' element;
|
changeset |
files
|
| Thu, 20 Nov 2008 00:03:53 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
changeset |
files
|
| Wed, 19 Nov 2008 18:15:31 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 19 Nov 2008 17:55:18 +0100 |
nipkow |
fixed
|
changeset |
files
|
| Wed, 19 Nov 2008 17:54:55 +0100 |
nipkow |
Added new fold operator and renamed the old oe to fold_image.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:04:29 +0100 |
ballarin |
Type inference for elements through syntax module.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:03:13 +0100 |
ballarin |
Use 'if' in connection with 'is_some' and 'the'.
|
changeset |
files
|
| Wed, 19 Nov 2008 17:00:00 +0100 |
ballarin |
Basic types not qualified.
|
changeset |
files
|
| Wed, 19 Nov 2008 16:58:33 +0100 |
ballarin |
Enable switching to new locales during session.
|
changeset |
files
|
| Wed, 19 Nov 2008 08:58:57 +0100 |
haftmann |
explicit inhabitance proof
|
changeset |
files
|
| Tue, 18 Nov 2008 22:25:36 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
changeset |
files
|
| Tue, 18 Nov 2008 22:25:30 +0100 |
wenzelm |
fulfill_proof/thm_proof: commuted lazyness;
|
changeset |
files
|
| Tue, 18 Nov 2008 21:17:14 +0100 |
krauss |
removed lemmas called lemma1 and lemma2
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:59 +0100 |
wenzelm |
force_proofs after cumulative use_thys;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:55 +0100 |
wenzelm |
signed_string_of_int for priorities;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:52 +0100 |
wenzelm |
added force_proofs;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:49 +0100 |
wenzelm |
added force_proofs (based on thms ever passed through enter_thms);
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:45 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:42 +0100 |
wenzelm |
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:25:10 +0100 |
wenzelm |
moved table of standard Isabelle symbols to isar-ref manual;
|
changeset |
files
|
| Tue, 18 Nov 2008 18:22:49 +0100 |
wenzelm |
added isabelle-implementation manual;
|
changeset |
files
|
| Tue, 18 Nov 2008 13:19:13 +0100 |
wenzelm |
disabled threads -- as advertized;
|
changeset |
files
|
| Tue, 18 Nov 2008 11:26:59 +0100 |
wenzelm |
changes by Fabian Immler:
|
changeset |
files
|
| Tue, 18 Nov 2008 09:41:23 +0100 |
ballarin |
Code for switching to new locales.
|
changeset |
files
|
| Tue, 18 Nov 2008 09:40:44 +0100 |
ballarin |
add_thmss
|
changeset |
files
|
| Tue, 18 Nov 2008 09:40:06 +0100 |
ballarin |
Activate elements moved to element.ML.
|
changeset |
files
|
| Tue, 18 Nov 2008 00:11:06 +0100 |
wenzelm |
finish: force proofs;
|
changeset |
files
|
| Mon, 17 Nov 2008 23:34:35 +0100 |
wenzelm |
finish_proof: undefined promises may occur here;
|
changeset |
files
|
| Mon, 17 Nov 2008 23:17:13 +0100 |
wenzelm |
tuned promise/fullfill;
|
changeset |
files
|
| Mon, 17 Nov 2008 23:17:11 +0100 |
wenzelm |
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:36:48 +0100 |
wenzelm |
removed Induct/Mutil.thy -- the file has been moved to AFP;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:28:46 +0100 |
wenzelm |
simplified thm_deps -- no need to build a graph datastructure;
|
changeset |
files
|
| Mon, 17 Nov 2008 21:13:48 +0100 |
wenzelm |
removed Induct/Mutil.thy -- the file has been moved to AFP;
|
changeset |
files
|
| Mon, 17 Nov 2008 17:25:02 +0100 |
nipkow |
-> AFP
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:27 +0100 |
haftmann |
explicit name morphism function for locale interpretation
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:26 +0100 |
haftmann |
Name.name_with_prefix (temporarily)
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:22 +0100 |
haftmann |
adjusted locale signature to *_cmd convention
|
changeset |
files
|
| Mon, 17 Nov 2008 17:00:21 +0100 |
haftmann |
whitespace tuning
|
changeset |
files
|
| Mon, 17 Nov 2008 14:03:39 +0100 |
ballarin |
Generic activation of locales.
|
changeset |
files
|
| Sun, 16 Nov 2008 22:12:44 +0100 |
wenzelm |
proof_body/pthm: removed redundant types field;
|
changeset |
files
|
| Sun, 16 Nov 2008 22:12:43 +0100 |
wenzelm |
put_name/thm_proof: promises are filled with fulfilled proofs;
|
changeset |
files
|
| Sun, 16 Nov 2008 22:12:41 +0100 |
wenzelm |
proof_body/pthm: removed redundant types field;
|
changeset |
files
|
| Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
changeset |
files
|
| Sun, 16 Nov 2008 18:19:27 +0100 |
berghofe |
- Corrected order of quantification over Frees.
|
changeset |
files
|
| Sun, 16 Nov 2008 18:18:45 +0100 |
berghofe |
Frees in PThms are now quantified in the order of their appearance in the
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:37 +0100 |
wenzelm |
adapted PThm and MinProof;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:36 +0100 |
wenzelm |
retrieve thm deps from proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:35 +0100 |
wenzelm |
retrieve thm deps from proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:32 +0100 |
wenzelm |
adapted PThm;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:30 +0100 |
wenzelm |
proof_of_term: removed obsolete disambiguisation table;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:29 +0100 |
wenzelm |
rewrite_proof: simplified simprocs (no name required);
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:27 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:25 +0100 |
wenzelm |
refined notion of derivation, consiting of promises and proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:23 +0100 |
wenzelm |
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:21 +0100 |
wenzelm |
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:20 +0100 |
wenzelm |
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:19 +0100 |
wenzelm |
name_of_thm: Proofterm.fold_proof_atoms;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:17 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:15 +0100 |
wenzelm |
clean: added HOL-Main;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:13 +0100 |
wenzelm |
rewrite_proof: simplified simprocs (no name required);
|
changeset |
files
|
| Sat, 15 Nov 2008 11:25:17 +0100 |
wenzelm |
multithreading support for polyml-5.2 actually disabled -- as advertized;
|
changeset |
files
|
| Fri, 14 Nov 2008 16:49:52 +0100 |
ballarin |
Initial part of locale reimplementation.
|
changeset |
files
|
| Fri, 14 Nov 2008 14:00:52 +0100 |
ballarin |
Made local_note_prefix public.
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:11 +0100 |
haftmann |
re-educated guess
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:09 +0100 |
haftmann |
Name.is_nothing
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:08 +0100 |
haftmann |
lemmas about dom and minus / insert
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:07 +0100 |
haftmann |
added length_unique operation for code generation
|
changeset |
files
|
| Thu, 13 Nov 2008 22:45:12 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Thu, 13 Nov 2008 22:44:40 +0100 |
wenzelm |
removed "includes" element (lost update?);
|
changeset |
files
|
| Thu, 13 Nov 2008 22:36:30 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|
| Thu, 13 Nov 2008 22:07:31 +0100 |
wenzelm |
added section "Explicit instantiation within a subgoal context";
|
changeset |
files
|
| Thu, 13 Nov 2008 22:06:36 +0100 |
wenzelm |
renamed "Rules" to "Object-level rules";
|
changeset |
files
|
| Thu, 13 Nov 2008 22:05:49 +0100 |
wenzelm |
more on basic tactics;
|
changeset |
files
|
| Thu, 13 Nov 2008 22:05:09 +0100 |
wenzelm |
basic ML reference for tactics;
|
changeset |
files
|
| Thu, 13 Nov 2008 22:04:19 +0100 |
wenzelm |
added section "Tactics";
|
changeset |
files
|
| Thu, 13 Nov 2008 22:03:26 +0100 |
wenzelm |
more contributors;
|
changeset |
files
|
| Thu, 13 Nov 2008 22:02:18 +0100 |
wenzelm |
separate section "Inspecting the syntax" for print_syntax;
|
changeset |
files
|
| Thu, 13 Nov 2008 22:01:30 +0100 |
wenzelm |
misc tuning of inner syntax;
|
changeset |
files
|
| Thu, 13 Nov 2008 22:00:39 +0100 |
wenzelm |
added inner lexical syntax, reusing outer one;
|
changeset |
files
|
| Thu, 13 Nov 2008 22:00:12 +0100 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:59:47 +0100 |
wenzelm |
tuned outer lexical syntax; fixed var/tvar: really need question marks here;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:59:02 +0100 |
wenzelm |
more tuning of Pure grammer;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:57:50 +0100 |
wenzelm |
updated and elaborated Pure grammer;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:57:20 +0100 |
wenzelm |
added Pure grammer (from old ref manual);
|
changeset |
files
|
| Thu, 13 Nov 2008 21:56:49 +0100 |
wenzelm |
mixfix annotations: verbatim for special symbols;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:56:23 +0100 |
wenzelm |
added section "The Pure grammar" (incomplete version, based on old ref manual);
|
changeset |
files
|
| Thu, 13 Nov 2008 21:54:51 +0100 |
wenzelm |
added section "Priority grammars" (variant from old ref manual);
|
changeset |
files
|
| Thu, 13 Nov 2008 21:53:54 +0100 |
wenzelm |
added section "Co-regularity of type classes and arities" (variant from old ref manual);
|
changeset |
files
|
| Thu, 13 Nov 2008 21:52:59 +0100 |
wenzelm |
minor tuning (according to old ref manual);
|
changeset |
files
|
| Thu, 13 Nov 2008 21:52:09 +0100 |
wenzelm |
misc tuning and rearrangement of section "Printing logical entities";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:50:57 +0100 |
wenzelm |
misc tuning and rearrangement of section "Printing logical entities";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:50:30 +0100 |
wenzelm |
fixed/tuned syntax for attribute "tagged";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:49:46 +0100 |
wenzelm |
added pretty printing options (from old ref manual);
|
changeset |
files
|
| Thu, 13 Nov 2008 21:48:19 +0100 |
wenzelm |
separate chapter "Inner syntax --- the term language";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:45:40 +0100 |
wenzelm |
updated/refined types of Isar language elements, removed special LaTeX macros;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:43:46 +0100 |
wenzelm |
unified use of declaration environment with IsarImplementation;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:41:04 +0100 |
wenzelm |
ignore ThyOutput.source flag;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:40:30 +0100 |
wenzelm |
added bind_thm, bind_thms;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:40:00 +0100 |
wenzelm |
tuned section "Incorporating ML code";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:38:44 +0100 |
wenzelm |
tuned section "Oracles";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:38:02 +0100 |
wenzelm |
tuned section arrangement;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:37:18 +0100 |
wenzelm |
moved section "Proof method expressions" to proof chapter;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:34:55 +0100 |
wenzelm |
more on mixfix annotations (updated material from old ref manual);
|
changeset |
files
|
| Thu, 13 Nov 2008 21:34:23 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:33:56 +0100 |
wenzelm |
moved section "Document preparation" to front;
|
changeset |
files
|
| Thu, 13 Nov 2008 21:33:15 +0100 |
wenzelm |
updated section "Markup via command tags";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:32:36 +0100 |
wenzelm |
renamed "formal comments" to "document comments";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:31:25 +0100 |
wenzelm |
renamed "formal comments" to "document comments";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:30:41 +0100 |
wenzelm |
tuned "Markup commands";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:29:19 +0100 |
wenzelm |
tuned intro of "Document preparation";
|
changeset |
files
|
| Thu, 13 Nov 2008 21:25:42 +0100 |
wenzelm |
reworked "Defining Theories";
|
changeset |
files
|
| Thu, 13 Nov 2008 17:56:36 +0100 |
haftmann |
removed Assert.thy
|
changeset |
files
|
| Thu, 13 Nov 2008 15:59:36 +0100 |
haftmann |
dropped superfluos eval_conv
|
changeset |
files
|
| Thu, 13 Nov 2008 15:59:33 +0100 |
haftmann |
moved assert to Heap_Monad.thy
|
changeset |
files
|
| Thu, 13 Nov 2008 15:58:38 +0100 |
haftmann |
simproc for let
|
changeset |
files
|
| Thu, 13 Nov 2008 15:58:37 +0100 |
haftmann |
improved handling of !!/==> for eval and normalization
|
changeset |
files
|
| Thu, 13 Nov 2008 14:19:10 +0100 |
haftmann |
proper name morphisms for locales
|
changeset |
files
|
| Thu, 13 Nov 2008 14:19:09 +0100 |
haftmann |
consider prefixes for name bindings of simprocs (a first approximation)
|
changeset |
files
|
| Thu, 13 Nov 2008 14:19:07 +0100 |
haftmann |
diagnostic output for name bindings
|
changeset |
files
|
| Thu, 13 Nov 2008 01:31:20 +0100 |
berghofe |
Some modifications in code for proving arities to make it work for datatype
|
changeset |
files
|
| Wed, 12 Nov 2008 17:23:22 +0100 |
krauss |
min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
|
changeset |
files
|
| Mon, 10 Nov 2008 19:42:22 +0100 |
haftmann |
restruced naming code in anticipation of introduction of name morphisms
|
changeset |
files
|
| Mon, 10 Nov 2008 19:42:21 +0100 |
haftmann |
more verbose element printing
|
changeset |
files
|
| Mon, 10 Nov 2008 19:42:20 +0100 |
haftmann |
clarified comment
|
changeset |
files
|
| Mon, 10 Nov 2008 17:38:23 +0100 |
berghofe |
Added support for parametric datatypes.
|
changeset |
files
|
| Mon, 10 Nov 2008 17:37:25 +0100 |
berghofe |
Streamlined functions for accessing information about atoms.
|
changeset |
files
|
| Mon, 10 Nov 2008 17:34:26 +0100 |
berghofe |
Some more functions for accessing information about atoms.
|
changeset |
files
|
| Mon, 10 Nov 2008 14:36:49 +0100 |
ballarin |
Made doc compatible with the system.
|
changeset |
files
|
| Mon, 10 Nov 2008 09:03:28 +0100 |
haftmann |
clarified verbatim vs. typewriter
|
changeset |
files
|
| Mon, 10 Nov 2008 08:18:58 +0100 |
haftmann |
using explicit interpretaton prefix in Name.binding (still on the surface)
|
changeset |
files
|
| Mon, 10 Nov 2008 08:18:57 +0100 |
haftmann |
explicit interpretation prefix in Name.binding
|
changeset |
files
|
| Mon, 10 Nov 2008 08:18:56 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 07 Nov 2008 08:57:15 +0100 |
haftmann |
exported codegen_preproc
|
changeset |
files
|
| Thu, 06 Nov 2008 12:30:49 +0100 |
ballarin |
Minor cleanup.
|
changeset |
files
|
| Thu, 06 Nov 2008 12:29:51 +0100 |
ballarin |
Keyword 'includes' gone.
|
changeset |
files
|
| Thu, 06 Nov 2008 11:52:50 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 06 Nov 2008 11:52:42 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Thu, 06 Nov 2008 10:05:48 +0100 |
nipkow |
Added second tiling example.
|
changeset |
files
|
| Thu, 06 Nov 2008 09:09:51 +0100 |
haftmann |
cleaned
|
changeset |
files
|
| Thu, 06 Nov 2008 09:09:49 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 06 Nov 2008 09:09:48 +0100 |
haftmann |
class morphism stemming from locale interpretation
|
changeset |
files
|
| Mon, 03 Nov 2008 14:15:25 +0100 |
haftmann |
improved verbatim mechanism
|
changeset |
files
|
| Fri, 31 Oct 2008 10:39:04 +0100 |
berghofe |
Theorem "_" is now stored with open derivation.
|
changeset |
files
|
| Fri, 31 Oct 2008 10:37:34 +0100 |
berghofe |
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
|
changeset |
files
|
| Fri, 31 Oct 2008 10:35:30 +0100 |
berghofe |
Replaced arbitrary by undefined.
|
changeset |
files
|
| Thu, 30 Oct 2008 10:57:45 +0100 |
ballarin |
Dropped context element 'includes'.
|
changeset |
files
|
| Wed, 29 Oct 2008 15:32:58 +0100 |
haftmann |
adapted to strict pattern discipline
|
changeset |
files
|
| Wed, 29 Oct 2008 11:33:40 +0100 |
haftmann |
explicit check for pattern discipline before code translation
|
changeset |
files
|
| Tue, 28 Oct 2008 17:53:46 +0100 |
ballarin |
Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
|
changeset |
files
|
| Tue, 28 Oct 2008 16:59:02 +0100 |
haftmann |
restored incremental code generation
|
changeset |
files
|
| Tue, 28 Oct 2008 16:59:01 +0100 |
haftmann |
slightly tuned
|
changeset |
files
|
| Tue, 28 Oct 2008 16:59:00 +0100 |
haftmann |
assert that no class parameter is used as constructor
|
changeset |
files
|
| Tue, 28 Oct 2008 16:58:59 +0100 |
haftmann |
cleanup code default attribute
|
changeset |
files
|
| Tue, 28 Oct 2008 12:29:57 +0100 |
haftmann |
removed includes
|
changeset |
files
|
| Tue, 28 Oct 2008 12:28:14 +0100 |
haftmann |
making SMLNJ happy
|
changeset |
files
|
| Tue, 28 Oct 2008 11:05:44 +0100 |
paulson |
The metis method no longer fails because the theorem is too trivial
|
changeset |
files
|
| Tue, 28 Oct 2008 11:03:07 +0100 |
ballarin |
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
|
changeset |
files
|
| Mon, 27 Oct 2008 18:14:34 +0100 |
paulson |
metis proof
|
changeset |
files
|
| Mon, 27 Oct 2008 16:23:54 +0100 |
ballarin |
New-style locale expressions with instantiation (new file expression.ML).
|
changeset |
files
|
| Mon, 27 Oct 2008 16:20:52 +0100 |
ballarin |
Hide path in constant name (workaround).
|
changeset |
files
|
| Mon, 27 Oct 2008 16:15:50 +0100 |
haftmann |
explicit history for equations; tuned
|
changeset |
files
|
| Mon, 27 Oct 2008 16:15:49 +0100 |
haftmann |
slightly tuned
|
changeset |
files
|
| Mon, 27 Oct 2008 16:15:48 +0100 |
haftmann |
added rudimentary code generation
|
changeset |
files
|
| Mon, 27 Oct 2008 16:15:47 +0100 |
haftmann |
sup_bot and inf_top
|
changeset |
files
|
| Mon, 27 Oct 2008 16:14:51 +0100 |
ballarin |
Extension of interface: declarations_of.
|
changeset |
files
|
| Fri, 24 Oct 2008 17:51:36 +0200 |
haftmann |
simplified user-defined class syntax
|
changeset |
files
|
| Fri, 24 Oct 2008 17:51:35 +0200 |
haftmann |
more clever module names for code generation
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:42 +0200 |
haftmann |
"fun" gained a more uniform status
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:40 +0200 |
haftmann |
simplified syntax for class parameters
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:39 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:37 +0200 |
haftmann |
new classes "top" and "bot"
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:36 +0200 |
haftmann |
tuned proof
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:35 +0200 |
haftmann |
more clever module name aliasses for code generation
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:34 +0200 |
haftmann |
"arbitrary" merely abbreviates undefined
|
changeset |
files
|
| Fri, 24 Oct 2008 17:48:33 +0200 |
haftmann |
subst is a proper axiom again
|
changeset |
files
|
| Fri, 24 Oct 2008 10:41:15 +0200 |
haftmann |
updated
|
changeset |
files
|
| Fri, 24 Oct 2008 10:41:13 +0200 |
haftmann |
explicit namings for generated code
|
changeset |
files
|
| Thu, 23 Oct 2008 16:07:03 +0200 |
wenzelm |
Thm.get_def;
|
changeset |
files
|
| Thu, 23 Oct 2008 15:28:39 +0200 |
wenzelm |
Thm.def_name;
|
changeset |
files
|
| Thu, 23 Oct 2008 15:28:08 +0200 |
wenzelm |
multithreading support only for polyml-5.2.1 or later;
|
changeset |
files
|
| Thu, 23 Oct 2008 15:28:05 +0200 |
wenzelm |
renamed get_axiom_i to axiom, removed obsolete get_axiom;
|
changeset |
files
|
| Thu, 23 Oct 2008 15:28:01 +0200 |
wenzelm |
renamed Thm.get_axiom_i to Thm.axiom;
|
changeset |
files
|
| Thu, 23 Oct 2008 14:22:16 +0200 |
wenzelm |
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
|
changeset |
files
|
| Thu, 23 Oct 2008 13:52:28 +0200 |
wenzelm |
adapted Susp.peek;
|
changeset |
files
|
| Thu, 23 Oct 2008 13:52:27 +0200 |
wenzelm |
thread-safe version, with non-critical evaluation;
|
changeset |
files
|
| Thu, 23 Oct 2008 13:52:26 +0200 |
wenzelm |
do not open Susp;
|
changeset |
files
|
| Thu, 23 Oct 2008 13:51:54 +0200 |
wenzelm |
switched parallel sessions to polyml-5.2.1;
|
changeset |
files
|
| Thu, 23 Oct 2008 00:24:31 +0200 |
wenzelm |
fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
|
changeset |
files
|
| Wed, 22 Oct 2008 21:25:00 +0200 |
wenzelm |
updated to 5.2.1;
|
changeset |
files
|
| Wed, 22 Oct 2008 14:15:48 +0200 |
haftmann |
prove_instantiation_exit combinators
|
changeset |
files
|
| Wed, 22 Oct 2008 14:15:47 +0200 |
haftmann |
added meet_sort_typ
|
changeset |
files
|
| Wed, 22 Oct 2008 14:15:46 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 22 Oct 2008 14:15:45 +0200 |
haftmann |
code identifier namings are no longer imperative
|
changeset |
files
|
| Wed, 22 Oct 2008 14:15:44 +0200 |
haftmann |
tuned typedef interface
|
changeset |
files
|
| Wed, 22 Oct 2008 14:15:43 +0200 |
haftmann |
slightly tuned
|
changeset |
files
|
| Wed, 22 Oct 2008 14:15:42 +0200 |
haftmann |
fixed
|
changeset |
files
|
| Tue, 21 Oct 2008 23:54:42 +0200 |
wenzelm |
less ambitious default for JEDIT_JAVA_OPTIONS;
|
changeset |
files
|
| Tue, 21 Oct 2008 22:21:28 +0200 |
wenzelm |
JEDIT_OPTIONS: moved -settings to interface script (more robust);
|
changeset |
files
|
| Tue, 21 Oct 2008 21:59:22 +0200 |
wenzelm |
make JEDIT_JAVA_OPTIONS and JEDIT_OPTIONS actually work;
|
changeset |
files
|
| Tue, 21 Oct 2008 21:22:31 +0200 |
berghofe |
Added nominal_inductive2.
|
changeset |
files
|
| Tue, 21 Oct 2008 21:22:02 +0200 |
berghofe |
Example for using the generalized version of nominal_inductive.
|
changeset |
files
|
| Tue, 21 Oct 2008 21:20:46 +0200 |
berghofe |
Added theory W.
|
changeset |
files
|
| Tue, 21 Oct 2008 21:20:17 +0200 |
berghofe |
More general, still experimental version of nominal_inductive for
|
changeset |
files
|
| Tue, 21 Oct 2008 21:18:54 +0200 |
berghofe |
Added nominal_inductive2.ML
|
changeset |
files
|
| Tue, 21 Oct 2008 20:18:45 +0200 |
wenzelm |
added jEdit settings;
|
changeset |
files
|
| Tue, 21 Oct 2008 20:18:07 +0200 |
wenzelm |
tuned usage line;
|
changeset |
files
|
| Tue, 21 Oct 2008 20:17:40 +0200 |
wenzelm |
Isabelle/jEdit interface wrapper.
|
changeset |
files
|
| Tue, 21 Oct 2008 16:53:10 +0200 |
wenzelm |
join results in isolation;
|
changeset |
files
|
| Tue, 21 Oct 2008 16:53:00 +0200 |
wenzelm |
join_results: allow CRITICAL join of finished futures;
|
changeset |
files
|
| Tue, 21 Oct 2008 16:52:59 +0200 |
wenzelm |
Future.join_result;
|
changeset |
files
|
| Tue, 21 Oct 2008 15:01:18 +0200 |
wenzelm |
added Future.enabled check;
|
changeset |
files
|
| Tue, 21 Oct 2008 15:01:16 +0200 |
wenzelm |
ThyOutput: export some auxiliary operations;
|
changeset |
files
|
| Mon, 20 Oct 2008 23:53:17 +0200 |
nipkow |
fixed proof
|
changeset |
files
|
| Mon, 20 Oct 2008 23:52:59 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Sun, 19 Oct 2008 21:20:55 +0200 |
berghofe |
Names of variables in perm_eqs are now chosen more carefully to avoid
|
changeset |
files
|
| Sun, 19 Oct 2008 21:19:27 +0200 |
berghofe |
- removed test_params from CodegenData (now in Pure/Tools/quickcheck.ML)
|
changeset |
files
|
| Sun, 19 Oct 2008 21:14:53 +0200 |
berghofe |
datatype_codegen now checks name of result type of constructor
|
changeset |
files
|
| Sun, 19 Oct 2008 20:09:37 +0200 |
wenzelm |
run a program in a modified environment;
|
changeset |
files
|
| Fri, 17 Oct 2008 10:39:39 +0200 |
wenzelm |
reactivated HOL-Matrix;
|
changeset |
files
|
| Fri, 17 Oct 2008 10:21:03 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 17 Oct 2008 10:14:38 +0200 |
haftmann |
filled remaining gaps
|
changeset |
files
|
| Fri, 17 Oct 2008 10:14:12 +0200 |
haftmann |
added type antiquotation
|
changeset |
files
|
| Thu, 16 Oct 2008 23:58:29 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Oct 2008 23:56:57 +0200 |
wenzelm |
added dep for Concurrent/ROOT.ML;
|
changeset |
files
|
| Thu, 16 Oct 2008 23:47:01 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Oct 2008 23:21:23 +0200 |
wenzelm |
removed Locales;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:45:08 +0200 |
wenzelm |
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:37 +0200 |
wenzelm |
added translations for SORT_CONSTRAINT
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:36 +0200 |
wenzelm |
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:35 +0200 |
wenzelm |
added make;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:34 +0200 |
wenzelm |
maintain sort occurrences of declared terms;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:33 +0200 |
wenzelm |
added weaken_sorts;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:32 +0200 |
wenzelm |
added make, minimal_sorts;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:31 +0200 |
wenzelm |
added const sort_constraint with syntax SORT_CONSTRAINT -- logically vacous;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:30 +0200 |
wenzelm |
added check_shyps, which reject pending sort hypotheses;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:29 +0200 |
wenzelm |
Drule.norm_hhf_eqs;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:28 +0200 |
wenzelm |
prove_common: include all sorts from context into statement, check shyps of result;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:27 +0200 |
wenzelm |
added rules for sort_constraint, include in norm_hhf_eqs;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:25 +0200 |
wenzelm |
avoid accidental dependency of automated proof on sort equiv;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:24 +0200 |
wenzelm |
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
|
changeset |
files
|
| Thu, 16 Oct 2008 22:44:22 +0200 |
wenzelm |
avoid CRITICAL with_path;
|
changeset |
files
|
| Thu, 16 Oct 2008 19:44:36 +0200 |
huffman |
rewrite more proofs in Isar style
|
changeset |
files
|
| Thu, 16 Oct 2008 17:52:54 +0200 |
ballarin |
Removed ex/Locales.thy.
|
changeset |
files
|
| Thu, 16 Oct 2008 17:19:47 +0200 |
ballarin |
More occurrences of 'includes' gone.
|
changeset |
files
|
| Thu, 16 Oct 2008 17:07:20 +0200 |
ballarin |
Removed outdated locales tutorial.
|
changeset |
files
|
| Thu, 16 Oct 2008 08:51:05 +0200 |
haftmann |
correct rounding
|
changeset |
files
|
| Thu, 16 Oct 2008 08:48:27 +0200 |
haftmann |
circumvent some TeX problem
|
changeset |
files
|
| Thu, 16 Oct 2008 00:18:53 +0200 |
kleing |
only test HOL image for smlnj
|
changeset |
files
|
| Wed, 15 Oct 2008 22:12:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 15 Oct 2008 21:45:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 15 Oct 2008 21:15:35 +0200 |
wenzelm |
generic ATP manager based on threads (by Fabian Immler);
|
changeset |
files
|
| Wed, 15 Oct 2008 21:06:15 +0200 |
wenzelm |
added sledgehammer etc.;
|
changeset |
files
|
| Wed, 15 Oct 2008 19:43:11 +0200 |
wenzelm |
removed obsolete Complex sessions;
|
changeset |
files
|
| Wed, 15 Oct 2008 16:25:31 +0200 |
haftmann |
figure for adaption
|
changeset |
files
|
| Wed, 15 Oct 2008 16:06:59 +0200 |
ballarin |
Removed 'includes' (fixed).
|
changeset |
files
|
| Wed, 15 Oct 2008 15:44:15 +0200 |
ballarin |
Removed 'includes'.
|
changeset |
files
|
| Wed, 15 Oct 2008 00:18:43 +0200 |
kleing |
give more time to do inital loggin and settings read
|
changeset |
files
|
| Wed, 15 Oct 2008 00:18:19 +0200 |
kleing |
log start of test session
|
changeset |
files
|
| Tue, 14 Oct 2008 20:10:45 +0200 |
wenzelm |
tuned interfaces -- plain prover function, without thread;
|
changeset |
files
|
| Tue, 14 Oct 2008 20:10:44 +0200 |
wenzelm |
add_prover: plain prover function, without thread;
|
changeset |
files
|
| Tue, 14 Oct 2008 20:10:43 +0200 |
wenzelm |
tuned AtpWrapper interfaces;
|
changeset |
files
|
| Tue, 14 Oct 2008 16:32:26 +0200 |
haftmann |
continued codegen tutorial
|
changeset |
files
|
| Tue, 14 Oct 2008 16:01:36 +0200 |
wenzelm |
renamed AtpThread to AtpWrapper;
|
changeset |
files
|
| Tue, 14 Oct 2008 15:45:46 +0200 |
wenzelm |
adding preferences is now permissive;
|
changeset |
files
|
| Tue, 14 Oct 2008 15:45:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 14 Oct 2008 15:45:44 +0200 |
wenzelm |
adding preferences is now permissive, no error handling here;
|
changeset |
files
|
| Tue, 14 Oct 2008 15:16:13 +0200 |
wenzelm |
CRITICAL access to preferences;
|
changeset |
files
|
| Tue, 14 Oct 2008 15:16:12 +0200 |
wenzelm |
export generic_pref etc.;
|
changeset |
files
|
| Tue, 14 Oct 2008 15:16:11 +0200 |
wenzelm |
renamed kill_all to kill, in conformance with atp_kill command;
|
changeset |
files
|
| Tue, 14 Oct 2008 15:16:09 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 14 Oct 2008 13:24:07 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Tue, 14 Oct 2008 13:23:31 +0200 |
nipkow |
Added liveness analysis
|
changeset |
files
|
| Tue, 14 Oct 2008 13:01:58 +0200 |
wenzelm |
info: back to plain printing;
|
changeset |
files
|
| Tue, 14 Oct 2008 13:01:57 +0200 |
wenzelm |
added min_elem, upto;
|
changeset |
files
|
| Tue, 14 Oct 2008 13:01:56 +0200 |
wenzelm |
added value;
|
changeset |
files
|
| Tue, 14 Oct 2008 13:01:52 +0200 |
wenzelm |
simplified synchronized variable access;
|
changeset |
files
|
| Mon, 13 Oct 2008 15:48:40 +0200 |
wenzelm |
State variables with synchronized access.
|
changeset |
files
|
| Mon, 13 Oct 2008 15:48:39 +0200 |
wenzelm |
added generic combinator for synchronized evaluation (formerly in future.ML);
|
changeset |
files
|
| Mon, 13 Oct 2008 15:48:38 +0200 |
wenzelm |
simplified implementation using Synchronized.var;
|
changeset |
files
|
| Mon, 13 Oct 2008 15:48:37 +0200 |
wenzelm |
SimpleThread.synchronized;
|
changeset |
files
|
| Mon, 13 Oct 2008 15:48:36 +0200 |
wenzelm |
added Concurrent/synchronized.ML;
|
changeset |
files
|
| Mon, 13 Oct 2008 14:04:53 +0200 |
wenzelm |
** Update from Fabian **
|
changeset |
files
|
| Mon, 13 Oct 2008 14:04:29 +0200 |
wenzelm |
** Update from Fabian **
|
changeset |
files
|
| Mon, 13 Oct 2008 14:04:28 +0200 |
wenzelm |
** Update from Fabian **
|
changeset |
files
|
| Mon, 13 Oct 2008 13:56:54 +0200 |
wenzelm |
tuned output;
|
changeset |
files
|
| Mon, 13 Oct 2008 13:44:59 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 13 Oct 2008 06:54:25 +0200 |
urbanc |
tuned
|
changeset |
files
|
| Sat, 11 Oct 2008 03:54:34 +0200 |
kleing |
change DISTPREFIX to not use yet another filesystem
|
changeset |
files
|
| Fri, 10 Oct 2008 16:02:15 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 10 Oct 2008 15:52:45 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 10 Oct 2008 15:23:33 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 10 Oct 2008 06:49:44 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
changeset |
files
|
| Fri, 10 Oct 2008 06:45:50 +0200 |
haftmann |
some adaption
|
changeset |
files
|
| Fri, 10 Oct 2008 06:45:49 +0200 |
haftmann |
using tikz pictures
|
changeset |
files
|
| Fri, 10 Oct 2008 06:45:48 +0200 |
haftmann |
tuned default rules of (dvd)
|
changeset |
files
|
| Thu, 09 Oct 2008 21:34:11 +0200 |
wenzelm |
replaced str_of by general peek;
|
changeset |
files
|
| Thu, 09 Oct 2008 21:34:05 +0200 |
wenzelm |
extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
|
changeset |
files
|
| Thu, 09 Oct 2008 21:06:08 +0200 |
wenzelm |
fixed spelling;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:24 +0200 |
wenzelm |
added enabled;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:23 +0200 |
wenzelm |
added enabled;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:22 +0200 |
wenzelm |
Multithreading.enabled;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:21 +0200 |
wenzelm |
moved future_scheduler flag to Concurrent/ROOT.ML;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:20 +0200 |
wenzelm |
added invalidate_group;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:17 +0200 |
wenzelm |
added fail-safe interrupt;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:16 +0200 |
wenzelm |
subject to Multithreading.enabled;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:15 +0200 |
wenzelm |
future result: Interrupt invalidates group, but pretends success otherwise;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:14 +0200 |
wenzelm |
added future_scheduler flag (tmp!), from skip_proofs.ML;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:13 +0200 |
wenzelm |
Dummy version of parallel list combinators -- plain sequential evaluation.
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:12 +0200 |
wenzelm |
added Concurrent/par_list_dummy.ML;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:11 +0200 |
wenzelm |
improved performance of skolem cache, due to parallel map;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:53:10 +0200 |
wenzelm |
SimpleThread.interrupt;
|
changeset |
files
|
| Thu, 09 Oct 2008 20:03:22 +0200 |
wenzelm |
report: back to single message;
|
changeset |
files
|
| Thu, 09 Oct 2008 19:24:21 +0200 |
wenzelm |
added section label;
|
changeset |
files
|
| Thu, 09 Oct 2008 18:16:07 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 09 Oct 2008 09:18:32 +0200 |
kleing |
do logging to MASTERLOG centrally (avoid multiple writers over NFS as
|
changeset |
files
|
| Thu, 09 Oct 2008 08:47:28 +0200 |
haftmann |
removed legacy |>>>
|
changeset |
files
|
| Thu, 09 Oct 2008 08:47:27 +0200 |
haftmann |
established canonical argument order in SML code generators
|
changeset |
files
|
| Thu, 09 Oct 2008 08:47:26 +0200 |
haftmann |
established canonical argument order
|
changeset |
files
|
| Thu, 09 Oct 2008 08:47:25 +0200 |
haftmann |
made SMLNJ happy
|
changeset |
files
|
| Wed, 08 Oct 2008 20:37:44 +0200 |
wenzelm |
less tracing;
|
changeset |
files
|
| Wed, 08 Oct 2008 20:21:35 +0200 |
wenzelm |
Future.joint_results is already uninterruptible;
|
changeset |
files
|
| Wed, 08 Oct 2008 20:21:34 +0200 |
wenzelm |
more careful handling of group interrupts;
|
changeset |
files
|
| Wed, 08 Oct 2008 19:32:20 +0200 |
wenzelm |
use polyml-cvs, which fixes a serious deadlock problem of Poly/ML runtime vs. GC;
|
changeset |
files
|
| Wed, 08 Oct 2008 19:30:15 +0200 |
wenzelm |
added HOL-Main;
|
changeset |
files
|
| Wed, 08 Oct 2008 19:20:29 +0200 |
wenzelm |
setmp_noncritical makes it work with future scheduler;
|
changeset |
files
|
| Wed, 08 Oct 2008 18:09:36 +0200 |
paulson |
The result of the equality inference rule no longer undergoes factoring.
|
changeset |
files
|
| Wed, 08 Oct 2008 00:25:38 +0200 |
kleing |
make the test for experimental sessions in isatest-check actually work
|
changeset |
files
|
| Wed, 08 Oct 2008 00:03:42 +0200 |
kleing |
leave a log message when no snapshot is generated
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:59 +0200 |
haftmann |
clarified preprocessor policies
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:50 +0200 |
haftmann |
arbitrary is undefined
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:40 +0200 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:33 +0200 |
haftmann |
only one theorem table for both code generators
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:30 +0200 |
haftmann |
proper default codegen attribute
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:25 +0200 |
haftmann |
tuned code setup
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:24 +0200 |
haftmann |
code generator more liberal with respect to sort constraints of instance parameters
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:23 +0200 |
haftmann |
more Isar for example
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:22 +0200 |
haftmann |
tuned funpow code generation
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:21 +0200 |
haftmann |
tuned min/max code generation
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:20 +0200 |
haftmann |
dropped superfluous if
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:18 +0200 |
haftmann |
tuned of_nat code generation
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:16 +0200 |
haftmann |
re-introduces axiom subst
|
changeset |
files
|
| Tue, 07 Oct 2008 16:07:14 +0200 |
haftmann |
corrected SML undefined
|
changeset |
files
|
| Tue, 07 Oct 2008 11:51:31 +0200 |
wenzelm |
updated to official version as of 07-Oct-2008;
|
changeset |
files
|
| Mon, 06 Oct 2008 22:41:21 +0200 |
wenzelm |
fold_lines: more tuning, avoiding extra split_last;
|
changeset |
files
|
| Mon, 06 Oct 2008 22:35:03 +0200 |
wenzelm |
extra check of PROOFGENERAL_HOME;
|
changeset |
files
|
| Sun, 05 Oct 2008 13:13:48 +0200 |
kleing |
needs -b option for isabelle getenv
|
changeset |
files
|
| Sat, 04 Oct 2008 17:51:10 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Sat, 04 Oct 2008 17:50:57 +0200 |
wenzelm |
tuned isabelle usage;
|
changeset |
files
|
| Sat, 04 Oct 2008 17:40:58 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Sat, 04 Oct 2008 17:40:56 +0200 |
wenzelm |
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
|
changeset |
files
|
| Sat, 04 Oct 2008 16:19:49 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Sat, 04 Oct 2008 16:19:00 +0200 |
wenzelm |
replaced ISABELLE by ISABELLE_PROCESS;
|
changeset |
files
|
| Sat, 04 Oct 2008 16:05:15 +0200 |
wenzelm |
ISABELLE_PROCESS commandline;
|
changeset |
files
|
| Sat, 04 Oct 2008 16:05:09 +0200 |
wenzelm |
replaced ISATOOL by ISABELLE_TOOL;
|
changeset |
files
|
| Sat, 04 Oct 2008 16:05:08 +0200 |
wenzelm |
ISABELLE_PROCESS replaces ISABELLE and ISABELLE_TOOL replaces ISATOOL -- old bindings stay for a while (legacy feature);
|
changeset |
files
|
| Sat, 04 Oct 2008 14:43:40 +0200 |
wenzelm |
eliminated prompt messages;
|
changeset |
files
|
| Sat, 04 Oct 2008 14:29:45 +0200 |
wenzelm |
added isabelle_tool version as basic integrity check of platform/distribution;
|
changeset |
files
|
| Sat, 04 Oct 2008 14:29:43 +0200 |
wenzelm |
renamed isatool to isabelle_tool in programming interfaces;
|
changeset |
files
|
| Sat, 04 Oct 2008 14:29:42 +0200 |
wenzelm |
Theory header keywords.
|
changeset |
files
|
| Sat, 04 Oct 2008 14:29:40 +0200 |
wenzelm |
added Thy/thy_header.scala;
|
changeset |
files
|
| Fri, 03 Oct 2008 21:31:27 +0200 |
wenzelm |
tuned quotes;
|
changeset |
files
|
| Fri, 03 Oct 2008 21:13:17 +0200 |
wenzelm |
factor: proper padding of digits;
|
changeset |
files
|
| Fri, 03 Oct 2008 21:06:39 +0200 |
wenzelm |
plain process_id function;
|
changeset |
files
|
| Fri, 03 Oct 2008 21:06:38 +0200 |
wenzelm |
removed obsolete Posix/Signal compatibility wrappers;
|
changeset |
files
|
| Fri, 03 Oct 2008 21:06:37 +0200 |
wenzelm |
removed obsolete Posix/Signal compatibility wrappers;
|
changeset |
files
|
| Fri, 03 Oct 2008 21:06:36 +0200 |
wenzelm |
removed obsolete Posix/Signal compatibility wrappers;
|
changeset |
files
|
| Fri, 03 Oct 2008 20:10:44 +0200 |
wenzelm |
do not handle Error (which matches arbitrary exceptions!), but ERROR _;
|
changeset |
files
|
| Fri, 03 Oct 2008 20:10:43 +0200 |
wenzelm |
updated to new AtpManager;
|
changeset |
files
|
| Fri, 03 Oct 2008 19:35:18 +0200 |
wenzelm |
operate on Proof.state, not Toplevel.state;
|
changeset |
files
|
| Fri, 03 Oct 2008 19:35:17 +0200 |
wenzelm |
misc simplifcation and tuning;
|
changeset |
files
|
| Fri, 03 Oct 2008 19:35:16 +0200 |
wenzelm |
perform atp_setups here;
|
changeset |
files
|
| Fri, 03 Oct 2008 19:35:15 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Fri, 03 Oct 2008 19:35:14 +0200 |
wenzelm |
removed HOL-Plain -- already included in HOL;
|
changeset |
files
|
| Fri, 03 Oct 2008 19:17:37 +0200 |
wenzelm |
removed spurious ResAtp.set_prover;
|
changeset |
files
|
| Fri, 03 Oct 2008 17:07:41 +0200 |
wenzelm |
simplified thread creation via SimpleThread;
|
changeset |
files
|
| Fri, 03 Oct 2008 17:07:39 +0200 |
wenzelm |
simplified thread creation via SimpleThread;
|
changeset |
files
|
| Fri, 03 Oct 2008 16:37:09 +0200 |
wenzelm |
version of sledgehammer using threads instead of processes, misc cleanup;
|
changeset |
files
|
| Fri, 03 Oct 2008 15:20:33 +0200 |
wenzelm |
removed old/unused setup of raw ATP oracles;
|
changeset |
files
|
| Fri, 03 Oct 2008 14:07:41 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 03 Oct 2008 14:06:19 +0200 |
wenzelm |
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
|
changeset |
files
|
| Fri, 03 Oct 2008 13:21:01 +0200 |
wenzelm |
added PROOFGENERAL_EMACS, with attempt to find Carbon Emacs;
|
changeset |
files
|
| Fri, 03 Oct 2008 00:21:48 +0200 |
wenzelm |
tuned tracing;
|
changeset |
files
|
| Fri, 03 Oct 2008 00:12:13 +0200 |
wenzelm |
slower heartbeat;
|
changeset |
files
|
| Thu, 02 Oct 2008 23:52:12 +0200 |
wenzelm |
added simple heartbeat thread;
|
changeset |
files
|
| Thu, 02 Oct 2008 23:52:10 +0200 |
wenzelm |
time factor: one more digit;
|
changeset |
files
|
| Thu, 02 Oct 2008 23:30:44 +0200 |
wenzelm |
more tuning of tracing messages;
|
changeset |
files
|
| Thu, 02 Oct 2008 22:09:22 +0200 |
wenzelm |
include factor in timing report;
|
changeset |
files
|
| Thu, 02 Oct 2008 21:21:21 +0200 |
wenzelm |
with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
|
changeset |
files
|
| Thu, 02 Oct 2008 19:59:01 +0200 |
wenzelm |
tracing: ignore failure of any kind;
|
changeset |
files
|
| Thu, 02 Oct 2008 19:59:00 +0200 |
wenzelm |
tuned SYNCHRONIZED: outermost Exn.release;
|
changeset |
files
|
| Thu, 02 Oct 2008 19:38:48 +0200 |
wenzelm |
program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
|
changeset |
files
|
| Thu, 02 Oct 2008 17:18:36 +0200 |
haftmann |
added partiality section
|
changeset |
files
|
| Thu, 02 Oct 2008 17:18:22 +0200 |
haftmann |
corrected class antiquotation
|
changeset |
files
|
| Thu, 02 Oct 2008 14:22:45 +0200 |
wenzelm |
max_threads_value always 1 for dummy version;
|
changeset |
files
|
| Thu, 02 Oct 2008 14:22:44 +0200 |
wenzelm |
simplified Exn.EXCEPTIONS, flatten nested occurrences;
|
changeset |
files
|
| Thu, 02 Oct 2008 14:22:40 +0200 |
wenzelm |
simplified Exn.EXCEPTIONS;
|
changeset |
files
|
| Thu, 02 Oct 2008 14:22:36 +0200 |
wenzelm |
major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
|
changeset |
files
|
| Thu, 02 Oct 2008 13:07:33 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 02 Oct 2008 12:17:20 +0200 |
berghofe |
Yet another proof of Newman's lemma, this time using the coherent logic prover.
|
changeset |
files
|
| Wed, 01 Oct 2008 22:33:29 +0200 |
wenzelm |
unit_source: more rigid parsing, stop after final qed;
|
changeset |
files
|
| Wed, 01 Oct 2008 22:33:28 +0200 |
wenzelm |
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
|
changeset |
files
|
| Wed, 01 Oct 2008 22:33:24 +0200 |
wenzelm |
replaced can_defer by is_relevant (negation);
|
changeset |
files
|
| Wed, 01 Oct 2008 20:02:37 +0200 |
wenzelm |
datatype transition: internal trans field is maintained in reverse order;
|
changeset |
files
|
| Wed, 01 Oct 2008 18:16:14 +0200 |
wenzelm |
future_proof: protect conclusion of deferred proof state;
|
changeset |
files
|
| Wed, 01 Oct 2008 18:16:10 +0200 |
wenzelm |
future_schedule: back to one group for all loader tasks;
|
changeset |
files
|
| Wed, 01 Oct 2008 14:17:06 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Wed, 01 Oct 2008 13:33:54 +0200 |
haftmann |
fixed
|
changeset |
files
|
| Wed, 01 Oct 2008 12:18:18 +0200 |
wenzelm |
renamed promise to future, tuned related interfaces;
|
changeset |
files
|
| Wed, 01 Oct 2008 12:00:05 +0200 |
wenzelm |
more robust treatment of Interrupt (cf. exn.ML);
|
changeset |
files
|
| Wed, 01 Oct 2008 12:00:04 +0200 |
wenzelm |
more robust treatment of Interrupt;
|
changeset |
files
|
| Wed, 01 Oct 2008 12:00:02 +0200 |
wenzelm |
more robust treatment of Interrupt (cf. exn.ML);
|
changeset |
files
|
| Wed, 01 Oct 2008 12:00:01 +0200 |
wenzelm |
removed release_results (cf. Exn.release_all, Exn.release_first);
|
changeset |
files
|
| Wed, 01 Oct 2008 12:00:00 +0200 |
wenzelm |
more precise join_futures, improved termination;
|
changeset |
files
|
| Wed, 01 Oct 2008 08:42:42 +0200 |
haftmann |
added more_antiquote.ML
|
changeset |
files
|
| Wed, 01 Oct 2008 00:09:51 +0200 |
kleing |
extract Isabelle dist name correctly
|
changeset |
files
|
| Tue, 30 Sep 2008 23:31:40 +0200 |
wenzelm |
unit_source: explicit treatment of 'oops' proofs;
|
changeset |
files
|
| Tue, 30 Sep 2008 23:31:38 +0200 |
wenzelm |
promise_proof: proper statement with empty vars;
|
changeset |
files
|
| Tue, 30 Sep 2008 23:31:36 +0200 |
wenzelm |
load_thy: more precise treatment of improper cmd or proof (notably 'oops');
|
changeset |
files
|
| Tue, 30 Sep 2008 22:02:55 +0200 |
wenzelm |
schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);
|
changeset |
files
|
| Tue, 30 Sep 2008 22:02:53 +0200 |
wenzelm |
added unit_source: commands with proof;
|
changeset |
files
|
| Tue, 30 Sep 2008 22:02:51 +0200 |
wenzelm |
begin_proof: avoid race condition wrt. skip_proofs flag;
|
changeset |
files
|
| Tue, 30 Sep 2008 22:02:50 +0200 |
wenzelm |
load_thy: Toplevel.excursion based on units of command/proof pairs;
|
changeset |
files
|
| Tue, 30 Sep 2008 22:02:47 +0200 |
wenzelm |
more command categories;
|
changeset |
files
|
| Tue, 30 Sep 2008 22:02:45 +0200 |
wenzelm |
renamed Future.fork_irrelevant to Future.fork_background;
|
changeset |
files
|
| Tue, 30 Sep 2008 22:02:44 +0200 |
wenzelm |
export explicit joint_futures, removed Theory.at_end hook;
|
changeset |
files
|
| Tue, 30 Sep 2008 14:30:44 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 30 Sep 2008 14:19:28 +0200 |
wenzelm |
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
|
changeset |
files
|
| Tue, 30 Sep 2008 14:19:27 +0200 |
wenzelm |
Toplevel.commit_exit: position;
|
changeset |
files
|
| Tue, 30 Sep 2008 14:19:26 +0200 |
wenzelm |
export setmp_thread_position;
|
changeset |
files
|
| Tue, 30 Sep 2008 14:19:25 +0200 |
wenzelm |
simplified process_file, eliminated Toplevel.excursion;
|
changeset |
files
|
| Tue, 30 Sep 2008 12:49:18 +0200 |
haftmann |
clarified codegen interfaces
|
changeset |
files
|
| Tue, 30 Sep 2008 12:49:17 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 30 Sep 2008 12:49:16 +0200 |
haftmann |
reorganized examples
|
changeset |
files
|
| Tue, 30 Sep 2008 12:49:14 +0200 |
haftmann |
fixed slips
|
changeset |
files
|
| Tue, 30 Sep 2008 11:19:47 +0200 |
haftmann |
re-canibalised manual
|
changeset |
files
|
| Tue, 30 Sep 2008 04:06:55 +0200 |
kleing |
slightly different command line for makedist_mercurial
|
changeset |
files
|
| Mon, 29 Sep 2008 21:45:44 +0200 |
wenzelm |
put_thms: ContextPosition.set_visible false;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:49 +0200 |
wenzelm |
added type pp, which helps installing polymorphic pretty printers;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:46 +0200 |
wenzelm |
added str_of;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:44 +0200 |
wenzelm |
install_pp Future.T (polyml only);
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:41 +0200 |
wenzelm |
report_token/parse_token: back to context-less version;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:39 +0200 |
wenzelm |
back to plain Position.report for regular references;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:36 +0200 |
wenzelm |
back to plain Position.report for regular references;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:32 +0200 |
wenzelm |
promise global proofs;
|
changeset |
files
|
| Mon, 29 Sep 2008 21:26:26 +0200 |
wenzelm |
renamed report to report_visible;
|
changeset |
files
|
| Mon, 29 Sep 2008 14:59:02 +0200 |
wenzelm |
code example: back to individual ML commands, which are now thread-safe;
|
changeset |
files
|
| Mon, 29 Sep 2008 14:41:25 +0200 |
wenzelm |
ContextPosition.report;
|
changeset |
files
|
| Mon, 29 Sep 2008 14:41:24 +0200 |
wenzelm |
target update: invisible context position avoids duplication of reports etc.;
|
changeset |
files
|
| Mon, 29 Sep 2008 14:41:23 +0200 |
wenzelm |
Context position visibility.
|
changeset |
files
|
| Mon, 29 Sep 2008 14:41:22 +0200 |
wenzelm |
added context_position.ML;
|
changeset |
files
|
| Mon, 29 Sep 2008 12:32:00 +0200 |
haftmann |
more precise redundancy check
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:59 +0200 |
haftmann |
clarified dependencies between arith tools
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:58 +0200 |
haftmann |
separate HOL-Main image
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:57 +0200 |
haftmann |
polished code generator setup
|
changeset |
files
|
| Mon, 29 Sep 2008 12:31:56 +0200 |
haftmann |
added theory antiquotation
|
changeset |
files
|
| Mon, 29 Sep 2008 11:46:52 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Mon, 29 Sep 2008 11:46:47 +0200 |
wenzelm |
handle _ should be avoided (spurious Interrupt will spoil the game);
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:04 +0200 |
wenzelm |
added norm_export_morphism;
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:03 +0200 |
wenzelm |
added exit_global, exit_result, exit_result_global;
|
changeset |
files
|
| Mon, 29 Sep 2008 10:58:01 +0200 |
wenzelm |
LocalTheory.exit_global;
|
changeset |
files
|
| Sun, 28 Sep 2008 14:46:51 +0200 |
wenzelm |
HOL no longer depends on HOL-Plain;
|
changeset |
files
|
| Sun, 28 Sep 2008 14:40:43 +0200 |
wenzelm |
setmp_noncritical;
|
changeset |
files
|
| Sun, 28 Sep 2008 12:42:35 +0200 |
wenzelm |
join earlier promises first;
|
changeset |
files
|
| Sun, 28 Sep 2008 12:23:45 +0200 |
wenzelm |
proper setmp_thread_data for nested execute (cf. join_loop);
|
changeset |
files
|
| Sun, 28 Sep 2008 12:23:44 +0200 |
wenzelm |
promise_result: enforce strictly sequential dependencies, via serial numbers;
|
changeset |
files
|
| Sun, 28 Sep 2008 09:25:24 +0200 |
kleing |
do not cvs update for doc test (switching to mercurial, update done outside
|
changeset |
files
|
| Sun, 28 Sep 2008 09:13:46 +0200 |
kleing |
use mercurial repository for isatest
|
changeset |
files
|
| Sun, 28 Sep 2008 00:00:55 +0200 |
wenzelm |
thread_data: include thread name, export access;
|
changeset |
files
|
| Sat, 27 Sep 2008 19:35:00 +0200 |
wenzelm |
setmp_noncritical;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:08 +0200 |
wenzelm |
dequeue_towards: return bound for unfinished tasks;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:07 +0200 |
wenzelm |
moved release_results to future.ML;
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:06 +0200 |
wenzelm |
added release_results (formerly in par_list.ML);
|
changeset |
files
|
| Sat, 27 Sep 2008 18:18:05 +0200 |
wenzelm |
Future.release_results;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:37:01 +0200 |
wenzelm |
more tracing;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:39 +0200 |
wenzelm |
Theory.checkpoint for main operations, admits concurrent proofs;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:37 +0200 |
wenzelm |
promise: include check into future body, i.e. joined results are always valid;
|
changeset |
files
|
| Sat, 27 Sep 2008 15:20:36 +0200 |
wenzelm |
proper transfer of theorems that involve classes being instantiated here;
|
changeset |
files
|
| Sat, 27 Sep 2008 14:26:06 +0200 |
wenzelm |
HOL_USEDIR_OPTIONS no longer applies to HOL-Plain (main HOL is rebuilt from Pure);
|
changeset |
files
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
changeset |
files
|
| Fri, 26 Sep 2008 17:24:15 +0200 |
wenzelm |
added subset operation;
|
changeset |
files
|
| Fri, 26 Sep 2008 14:53:10 +0200 |
berghofe |
Added fresh_star_const.
|
changeset |
files
|
| Fri, 26 Sep 2008 14:52:27 +0200 |
berghofe |
Added some more theorems to NominalData.
|
changeset |
files
|
| Fri, 26 Sep 2008 14:51:27 +0200 |
berghofe |
Added some more lemmas that are useful in proof of strong induction rule.
|
changeset |
files
|
| Fri, 26 Sep 2008 09:10:02 +0200 |
haftmann |
removed obsolete name convention "func"
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:53 +0200 |
haftmann |
fixed typo
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:52 +0200 |
haftmann |
clarified function transformator interface
|
changeset |
files
|
| Fri, 26 Sep 2008 09:09:51 +0200 |
haftmann |
op = vs. eq
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:21 +0200 |
wenzelm |
moved future_scheduler flag to skip_proof.ML;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:20 +0200 |
wenzelm |
added future_scheduler (from thy_info.ML);
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:19 +0200 |
wenzelm |
simplified promise;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:18 +0200 |
wenzelm |
simplified Thm.promise;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:17 +0200 |
wenzelm |
explicit checkpoint for low-level (global) theory operations admits concurrent SkipProof.prove;
|
changeset |
files
|
| Thu, 25 Sep 2008 20:34:15 +0200 |
wenzelm |
explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
|
changeset |
files
|
| Thu, 25 Sep 2008 19:15:50 +0200 |
haftmann |
circumvent problem with code redundancy
|
changeset |
files
|
| Thu, 25 Sep 2008 16:05:52 +0200 |
haftmann |
clarifed redundancy policy
|
changeset |
files
|
| Thu, 25 Sep 2008 14:37:32 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 25 Sep 2008 14:35:03 +0200 |
wenzelm |
added release_results;
|
changeset |
files
|
| Thu, 25 Sep 2008 14:35:02 +0200 |
wenzelm |
abtract types: plain datatype with opaque signature matching;
|
changeset |
files
|
| Thu, 25 Sep 2008 14:35:01 +0200 |
wenzelm |
prove: error with original thread position;
|
changeset |
files
|
| Thu, 25 Sep 2008 13:21:13 +0200 |
wenzelm |
explicit type OrdList.T;
|
changeset |
files
|
| Thu, 25 Sep 2008 11:14:01 +0200 |
haftmann |
(temporary workaround)
|
changeset |
files
|
| Thu, 25 Sep 2008 10:17:23 +0200 |
haftmann |
(temporal deactivation)
|
changeset |
files
|
| Thu, 25 Sep 2008 10:17:22 +0200 |
haftmann |
non left-linear equations for nbe
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:08 +0200 |
haftmann |
non left-linear equations for nbe
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:07 +0200 |
haftmann |
map_force
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:06 +0200 |
haftmann |
matchess
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:05 +0200 |
haftmann |
burrow_fst
|
changeset |
files
|
| Thu, 25 Sep 2008 09:28:03 +0200 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
changeset |
files
|
| Wed, 24 Sep 2008 19:39:25 +0200 |
wenzelm |
report: produce individual status messages;
|
changeset |
files
|
| Wed, 24 Sep 2008 19:33:14 +0200 |
wenzelm |
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
|
changeset |
files
|
| Wed, 24 Sep 2008 19:33:13 +0200 |
wenzelm |
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
|
changeset |
files
|
| Wed, 24 Sep 2008 18:08:42 +0200 |
wenzelm |
init: OuterKeyword.report;
|
changeset |
files
|
| Tue, 23 Sep 2008 23:07:48 +0200 |
wenzelm |
prove_multi: immediate;
|
changeset |
files
|
| Tue, 23 Sep 2008 22:04:30 +0200 |
wenzelm |
added promise_result, prove_promise;
|
changeset |
files
|
| Tue, 23 Sep 2008 18:31:33 +0200 |
berghofe |
Corrected call of SUBPROOF in coherent_tac that used wrong context.
|
changeset |
files
|
| Tue, 23 Sep 2008 18:11:45 +0200 |
haftmann |
fixed outer syntax
|
changeset |
files
|
| Tue, 23 Sep 2008 18:11:44 +0200 |
haftmann |
case default fallback for NBE
|
changeset |
files
|
| Tue, 23 Sep 2008 18:11:43 +0200 |
haftmann |
fixed quickcheck parameter syntax
|
changeset |
files
|
| Tue, 23 Sep 2008 18:11:42 +0200 |
haftmann |
renamed rtype to typerep
|
changeset |
files
|
| Tue, 23 Sep 2008 17:28:58 +0200 |
wenzelm |
added fold_rev;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:55 +0200 |
wenzelm |
added del_node, which is more efficient for sparse graphs;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:54 +0200 |
wenzelm |
IntGraph.del_node;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:53 +0200 |
wenzelm |
join_results: special case for empty list, works without multithreading;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:52 +0200 |
wenzelm |
added dest_deriv, removed external type deriv;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:51 +0200 |
wenzelm |
added conditional add_oracles, keep oracles_of_proof private;
|
changeset |
files
|
| Tue, 23 Sep 2008 15:48:50 +0200 |
wenzelm |
Thm.proof_of;
|
changeset |
files
|
| Mon, 22 Sep 2008 23:04:35 +0200 |
berghofe |
Added coherent logic prover.
|
changeset |
files
|
| Mon, 22 Sep 2008 23:01:54 +0200 |
berghofe |
New prover for coherent logic.
|
changeset |
files
|
| Mon, 22 Sep 2008 23:00:15 +0200 |
berghofe |
Added setup for coherent logic prover.
|
changeset |
files
|
| Mon, 22 Sep 2008 22:59:35 +0200 |
berghofe |
Added examples for coherent logic prover.
|
changeset |
files
|
| Mon, 22 Sep 2008 22:59:11 +0200 |
berghofe |
Examples for coherent logic prover.
|
changeset |
files
|
| Mon, 22 Sep 2008 19:46:24 +0200 |
urbanc |
made the perm_simp tactic to understand options such as (no_asm)
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:14 +0200 |
wenzelm |
type thm: fully internal derivation, no longer exported;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:14 +0200 |
wenzelm |
added is_finished;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:13 +0200 |
wenzelm |
added Promise constructor, which is similar to Oracle but may be replaced later;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:11 +0200 |
wenzelm |
removed deriv.ML which is now incorporated into thm.ML;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:11 +0200 |
wenzelm |
added reject_draft;
|
changeset |
files
|
| Mon, 22 Sep 2008 15:26:07 +0200 |
wenzelm |
type thm: fully internal derivation, no longer exported;
|
changeset |
files
|
| Mon, 22 Sep 2008 13:56:04 +0200 |
haftmann |
generic quickcheck framework
|
changeset |
files
|
| Mon, 22 Sep 2008 13:56:03 +0200 |
haftmann |
TEMPORARY: make batch run happy
|
changeset |
files
|
| Mon, 22 Sep 2008 13:56:01 +0200 |
haftmann |
absolute Library path
|
changeset |
files
|
| Mon, 22 Sep 2008 13:55:59 +0200 |
haftmann |
different session branches for HOL-Plain vs. Plain
|
changeset |
files
|
| Mon, 22 Sep 2008 08:00:28 +0200 |
haftmann |
temporary workaround for class constants
|
changeset |
files
|
| Mon, 22 Sep 2008 08:00:27 +0200 |
haftmann |
corrected sort intersection
|
changeset |
files
|
| Mon, 22 Sep 2008 08:00:26 +0200 |
haftmann |
some steps towards generic quickcheck framework
|
changeset |
files
|
| Mon, 22 Sep 2008 08:00:24 +0200 |
haftmann |
fixed headers
|
changeset |
files
|
| Mon, 22 Sep 2008 08:00:23 +0200 |
haftmann |
added some fragments from website
|
changeset |
files
|
| Sat, 20 Sep 2008 21:05:41 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 19 Sep 2008 22:11:50 +0200 |
wenzelm |
Isar toplevel editor model.
|
changeset |
files
|
| Fri, 19 Sep 2008 21:22:31 +0200 |
wenzelm |
future tasks: support boolean priorities (true = high, false = low/irrelevant);
|
changeset |
files
|
| Fri, 19 Sep 2008 21:00:50 +0200 |
wenzelm |
output_sync is now public;
|
changeset |
files
|
| Fri, 19 Sep 2008 21:00:49 +0200 |
wenzelm |
added props_text (from isar_syn.ML);
|
changeset |
files
|
| Fri, 19 Sep 2008 21:00:48 +0200 |
wenzelm |
moved Isar editor commands from isar_syn.ML to isar.ML;
|
changeset |
files
|
| Fri, 19 Sep 2008 21:00:47 +0200 |
wenzelm |
moved Isar editor commands from isar_syn.ML to isar.ML;
|
changeset |
files
|
| Fri, 19 Sep 2008 21:00:46 +0200 |
wenzelm |
added Isar/isar.scala;
|
changeset |
files
|
| Fri, 19 Sep 2008 18:05:19 +0200 |
huffman |
avoid using implicit assumptions
|
changeset |
files
|
| Fri, 19 Sep 2008 17:54:04 +0200 |
huffman |
add theory graph to ZF document
|
changeset |
files
|
| Fri, 19 Sep 2008 09:41:17 +0200 |
haftmann |
made SMLNJ happy
|
changeset |
files
|
| Thu, 18 Sep 2008 22:30:17 +0200 |
wenzelm |
jar: include sources;
|
changeset |
files
|
| Thu, 18 Sep 2008 20:12:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 18 Sep 2008 19:39:50 +0200 |
wenzelm |
eval_term: CRITICAL due to eval_result;
|
changeset |
files
|
| Thu, 18 Sep 2008 19:39:49 +0200 |
wenzelm |
begin_theory: Theory.checkpoint for immediate uses ensures that ML evaluation always starts with non-draft @{theory};
|
changeset |
files
|
| Thu, 18 Sep 2008 19:39:47 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
changeset |
files
|
| Thu, 18 Sep 2008 14:06:58 +0200 |
wenzelm |
show: non-critical testing;
|
changeset |
files
|
| Thu, 18 Sep 2008 14:06:56 +0200 |
wenzelm |
added deriv.ML: Abstract derivations based on raw proof terms.
|
changeset |
files
|
| Thu, 18 Sep 2008 12:13:50 +0200 |
krauss |
termination prover for "fun" can be configured using context data.
|
changeset |
files
|
| Thu, 18 Sep 2008 10:57:30 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Thu, 18 Sep 2008 10:57:23 +0200 |
wenzelm |
unchecked $ISABELLE_HOME_USER/etc/settings;
|
changeset |
files
|
| Wed, 17 Sep 2008 23:44:31 +0200 |
wenzelm |
use_text/use_file now depend on explicit ML name space;
|
changeset |
files
|
| Wed, 17 Sep 2008 23:23:49 +0200 |
wenzelm |
threads work only for Poly/ML 5.2 or later;
|
changeset |
files
|
| Wed, 17 Sep 2008 23:23:13 +0200 |
wenzelm |
* ML bindings produced via Isar commands are stored within the Isar context.
|
changeset |
files
|
| Wed, 17 Sep 2008 23:08:06 +0200 |
wenzelm |
added ML_prf;
|
changeset |
files
|
| Wed, 17 Sep 2008 23:04:27 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Wed, 17 Sep 2008 22:06:59 +0200 |
wenzelm |
added inherit_env;
|
changeset |
files
|
| Wed, 17 Sep 2008 22:06:57 +0200 |
wenzelm |
added map_contexts;
|
changeset |
files
|
| Wed, 17 Sep 2008 22:06:54 +0200 |
wenzelm |
ML_prf: inherit env for all contexts within the proof;
|
changeset |
files
|
| Wed, 17 Sep 2008 22:06:52 +0200 |
wenzelm |
shutdown only if Multithreading.available;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:44 +0200 |
wenzelm |
ML_Context.evaluate: proper context (for ML environment);
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:43 +0200 |
wenzelm |
ML_Context.evaluate: proper context (for ML environment);
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:38 +0200 |
wenzelm |
simplified ML_Context.eval_in -- expect immutable Proof.context value;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:36 +0200 |
wenzelm |
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:34 +0200 |
wenzelm |
simplified ML_Context.eval_in -- expect immutable Proof.context value;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:32 +0200 |
wenzelm |
explicit handling of ML environment within generic context;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:31 +0200 |
wenzelm |
added ML_prf;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:24 +0200 |
wenzelm |
use_text/use_file now depend on explicit ML name space;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:22 +0200 |
wenzelm |
ML name space -- dummy version of Poly/ML 5.2 facility.
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:20 +0200 |
wenzelm |
added ML-Systems/ml_name_space.ML;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:18 +0200 |
wenzelm |
use ML_prf within proofs;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:17 +0200 |
wenzelm |
local @{context};
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:14 +0200 |
wenzelm |
moved global ML bindings to global place;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:08 +0200 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
changeset |
files
|
| Wed, 17 Sep 2008 21:27:03 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Wed, 17 Sep 2008 15:59:23 +0200 |
krauss |
wf_finite_psubset[simp], in_finite_psubset[simp]
|
changeset |
files
|
| Wed, 17 Sep 2008 15:21:30 +0200 |
ballarin |
Public interface to interpretation morphism.
|
changeset |
files
|
| Wed, 17 Sep 2008 11:42:25 +0200 |
haftmann |
moved term_of syntax to separate theory
|
changeset |
files
|
| Wed, 17 Sep 2008 10:00:16 +0200 |
haftmann |
removed obsolete theory
|
changeset |
files
|
| Wed, 17 Sep 2008 07:32:04 +0200 |
haftmann |
added quickcheck.ML
|
changeset |
files
|
| Tue, 16 Sep 2008 18:01:25 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 16 Sep 2008 18:01:24 +0200 |
wenzelm |
multithreading for Poly/ML 5.1 is no longer supported;
|
changeset |
files
|
| Tue, 16 Sep 2008 17:28:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 16 Sep 2008 17:21:14 +0200 |
wenzelm |
updated system manual;
|
changeset |
files
|
| Tue, 16 Sep 2008 17:18:41 +0200 |
wenzelm |
Proof General / Emacs interface wrapper;
|
changeset |
files
|
| Tue, 16 Sep 2008 17:16:28 +0200 |
wenzelm |
Proof General: option -I is obsolete;
|
changeset |
files
|
| Tue, 16 Sep 2008 17:16:27 +0200 |
wenzelm |
added PROOFGENERAL_HOME;
|
changeset |
files
|
| Tue, 16 Sep 2008 17:16:25 +0200 |
wenzelm |
separate emacs tool for Proof General / Emacs;
|
changeset |
files
|
| Tue, 16 Sep 2008 16:13:31 +0200 |
haftmann |
added quickcheck stub
|
changeset |
files
|
| Tue, 16 Sep 2008 16:13:14 +0200 |
haftmann |
removed babel again
|
changeset |
files
|
| Tue, 16 Sep 2008 16:13:11 +0200 |
haftmann |
celver code lemma avoid type ambiguity problem with Haskell
|
changeset |
files
|
| Tue, 16 Sep 2008 16:13:09 +0200 |
haftmann |
a sophisticated char/nibble conversion combinator
|
changeset |
files
|
| Tue, 16 Sep 2008 16:13:06 +0200 |
haftmann |
moved term_of syntax to separate theory
|
changeset |
files
|
| Tue, 16 Sep 2008 15:37:33 +0200 |
wenzelm |
SimpleThread.fork;
|
changeset |
files
|
| Tue, 16 Sep 2008 15:37:32 +0200 |
wenzelm |
Simplified thread fork interface.
|
changeset |
files
|
| Tue, 16 Sep 2008 15:37:30 +0200 |
wenzelm |
added Concurrent/simple_thread.ML;
|
changeset |
files
|
| Tue, 16 Sep 2008 14:48:51 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 16 Sep 2008 14:40:30 +0200 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Tue, 16 Sep 2008 14:39:56 +0200 |
wenzelm |
check setting and tool;
|
changeset |
files
|
| Tue, 16 Sep 2008 12:27:05 +0200 |
ballarin |
Clearer separation of interpretation frontend and backend.
|
changeset |
files
|
| Tue, 16 Sep 2008 12:26:15 +0200 |
ballarin |
No interpretation of locale with dangling type frees.
|
changeset |
files
|
| Tue, 16 Sep 2008 12:25:26 +0200 |
ballarin |
Do not rely on locale assumption in interpretation.
|
changeset |
files
|
| Tue, 16 Sep 2008 12:25:04 +0200 |
paulson |
The metis method now fails in the usual manner, rather than raising an exception,
|
changeset |
files
|
| Tue, 16 Sep 2008 12:24:37 +0200 |
ballarin |
Fixed typo in locale declaration.
|
changeset |
files
|
| Tue, 16 Sep 2008 09:21:28 +0200 |
haftmann |
added babel
|
changeset |
files
|
| Tue, 16 Sep 2008 09:21:27 +0200 |
haftmann |
explicit size of characters
|
changeset |
files
|
| Tue, 16 Sep 2008 09:21:26 +0200 |
haftmann |
dropped superfluous code lemmas
|
changeset |
files
|
| Tue, 16 Sep 2008 09:21:24 +0200 |
haftmann |
evaluation using code generator
|
changeset |
files
|
| Tue, 16 Sep 2008 09:21:22 +0200 |
haftmann |
generic value command
|
changeset |
files
|
| Mon, 15 Sep 2008 20:51:58 +0200 |
wenzelm |
converted symbols.tex;
|
changeset |
files
|
| Mon, 15 Sep 2008 20:51:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 15 Sep 2008 20:22:38 +0200 |
wenzelm |
converted misc.tex;
|
changeset |
files
|
| Mon, 15 Sep 2008 19:43:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 15 Sep 2008 19:42:51 +0200 |
wenzelm |
generated files;
|
changeset |
files
|
| Mon, 15 Sep 2008 19:42:22 +0200 |
wenzelm |
converted present.tex;
|
changeset |
files
|
| Mon, 15 Sep 2008 17:32:12 +0200 |
wenzelm |
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
|
changeset |
files
|
| Mon, 15 Sep 2008 16:50:35 +0200 |
wenzelm |
load underscore package after iman etc.;
|
changeset |
files
|
| Mon, 15 Sep 2008 16:43:53 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Mon, 15 Sep 2008 16:43:31 +0200 |
wenzelm |
added formal markup for setting, executable, tool;
|
changeset |
files
|
| Mon, 15 Sep 2008 16:42:09 +0200 |
wenzelm |
basic setup for generated document sources (cf. IsarRef/isar-ref.tex);
|
changeset |
files
|
| Mon, 15 Sep 2008 16:42:00 +0200 |
wenzelm |
converted basics.tex to theory file;
|
changeset |
files
|
| Mon, 15 Sep 2008 16:40:53 +0200 |
wenzelm |
added isatt markup;
|
changeset |
files
|
| Sun, 14 Sep 2008 21:50:35 +0200 |
haftmann |
New outline for codegen tutorial -- draft
|
changeset |
files
|
| Fri, 12 Sep 2008 12:04:20 +0200 |
wenzelm |
added extern_fact (local or global);
|
changeset |
files
|
| Fri, 12 Sep 2008 12:04:19 +0200 |
wenzelm |
print raw (internal) result names;
|
changeset |
files
|
| Fri, 12 Sep 2008 12:04:16 +0200 |
wenzelm |
more procise printing of fact names;
|
changeset |
files
|
| Fri, 12 Sep 2008 10:54:00 +0200 |
wenzelm |
pretty_fact: extern fact name wrt. the given context, assuming that is the proper one for presentation;
|
changeset |
files
|
| Thu, 11 Sep 2008 22:22:59 +0200 |
wenzelm |
cancel, shutdown: notify_all;
|
changeset |
files
|
| Thu, 11 Sep 2008 22:22:20 +0200 |
wenzelm |
finish: Future.shutdown last;
|
changeset |
files
|
| Thu, 11 Sep 2008 21:53:53 +0200 |
wenzelm |
eliminated requests, use global state variables uniformly;
|
changeset |
files
|
| Thu, 11 Sep 2008 21:04:09 +0200 |
wenzelm |
finish: Future.shutdown;
|
changeset |
files
|
| Thu, 11 Sep 2008 21:04:07 +0200 |
wenzelm |
added is_empty;
|
changeset |
files
|
| Thu, 11 Sep 2008 21:04:05 +0200 |
wenzelm |
shutdown: global join-and-shutdown operation;
|
changeset |
files
|
| Thu, 11 Sep 2008 18:07:58 +0200 |
wenzelm |
added focus, which indicates a particular collection of high-priority tasks;
|
changeset |
files
|
| Thu, 11 Sep 2008 13:43:42 +0200 |
wenzelm |
some general notes on future values;
|
changeset |
files
|
| Thu, 11 Sep 2008 13:24:19 +0200 |
wenzelm |
separate Concurrent/ROOT.ML;
|
changeset |
files
|
| Thu, 11 Sep 2008 13:24:14 +0200 |
wenzelm |
Parallel list combinators.
|
changeset |
files
|
| Thu, 11 Sep 2008 13:23:57 +0200 |
wenzelm |
added Concurrent/par_list.ML;
|
changeset |
files
|
| Wed, 10 Sep 2008 23:28:09 +0200 |
wenzelm |
added interrupt_task (external id);
|
changeset |
files
|
| Wed, 10 Sep 2008 23:19:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 10 Sep 2008 22:29:36 +0200 |
wenzelm |
future_schedule: uninterruptible join;
|
changeset |
files
|
| Wed, 10 Sep 2008 21:50:32 +0200 |
wenzelm |
added future_scheduler (default false);
|
changeset |
files
|
| Wed, 10 Sep 2008 21:50:30 +0200 |
wenzelm |
replaced join_all by join_results, which returns Exn.results;
|
changeset |
files
|
| Wed, 10 Sep 2008 20:28:01 +0200 |
wenzelm |
workers: explicit activity flag;
|
changeset |
files
|
| Wed, 10 Sep 2008 19:44:29 +0200 |
wenzelm |
future: allow explicit group;
|
changeset |
files
|
| Wed, 10 Sep 2008 19:44:28 +0200 |
wenzelm |
cancel: invalidate group implicitly, via bool ref;
|
changeset |
files
|
| Wed, 10 Sep 2008 11:36:37 +0200 |
wenzelm |
auto_flush: uniform block buffering for all output streams;
|
changeset |
files
|
| Tue, 09 Sep 2008 23:48:38 +0200 |
wenzelm |
auto_flush stdout, stderr as well;
|
changeset |
files
|
| Tue, 09 Sep 2008 23:48:36 +0200 |
wenzelm |
proper values of no_interrupts, regular_interrupts;
|
changeset |
files
|
| Tue, 09 Sep 2008 23:30:05 +0200 |
wenzelm |
cancel: check_scheduler;
|
changeset |
files
|
| Tue, 09 Sep 2008 23:30:00 +0200 |
wenzelm |
simplified dequeue: provide Thread.self internally;
|
changeset |
files
|
| Tue, 09 Sep 2008 20:22:40 +0200 |
wenzelm |
eliminated cache, access queue efficiently via IntGraph.get_first;
|
changeset |
files
|
| Tue, 09 Sep 2008 20:22:30 +0200 |
wenzelm |
export get_first from underlying table;
|
changeset |
files
|
| Tue, 09 Sep 2008 19:57:54 +0200 |
wenzelm |
out_stream: block-buffered, with separate autoflush thread (every 50ms);
|
changeset |
files
|
| Tue, 09 Sep 2008 19:36:21 +0200 |
wenzelm |
babel: removed unnecessary "french" option, which actually enables french section names etc. on some LaTeX installations;
|
changeset |
files
|
| Tue, 09 Sep 2008 19:33:22 +0200 |
nipkow |
added comment
|
changeset |
files
|
| Tue, 09 Sep 2008 16:59:48 +0200 |
wenzelm |
human-readable printing of TaskQueue.task/group;
|
changeset |
files
|
| Tue, 09 Sep 2008 16:35:57 +0200 |
wenzelm |
* Changed defaults for unify configuration options;
|
changeset |
files
|
| Tue, 09 Sep 2008 16:29:34 +0200 |
wenzelm |
inherit group from running thread, or create a new one -- make it harder to re-use canceled groups;
|
changeset |
files
|
| Tue, 09 Sep 2008 16:29:32 +0200 |
wenzelm |
job: explicit 'ok' status -- false for canceled jobs;
|
changeset |
files
|
| Tue, 09 Sep 2008 16:17:08 +0200 |
paulson |
Overall exception handler in order to insulate our users from low-level bugs.
|
changeset |
files
|
| Tue, 09 Sep 2008 16:16:20 +0200 |
paulson |
more careful exception handling in order to prevent backtracking; miscellaneous tidying up.
|
changeset |
files
|
| Tue, 09 Sep 2008 16:15:25 +0200 |
paulson |
Increasing the default limits in order to prevent unnecessary failures.
|
changeset |
files
|
| Mon, 08 Sep 2008 22:14:39 +0200 |
wenzelm |
send: broadcast condition while locked!
|
changeset |
files
|
| Mon, 08 Sep 2008 21:08:30 +0200 |
wenzelm |
proper signature constraint;
|
changeset |
files
|
| Mon, 08 Sep 2008 20:35:38 +0200 |
wenzelm |
tuned Mailbox.send;
|
changeset |
files
|
| Mon, 08 Sep 2008 20:33:29 +0200 |
wenzelm |
removed unused sync_interrupts;
|
changeset |
files
|
| Mon, 08 Sep 2008 20:33:27 +0200 |
wenzelm |
moved thread data to future.ML (again);
|
changeset |
files
|
| Mon, 08 Sep 2008 20:33:24 +0200 |
wenzelm |
more interrupt operations;
|
changeset |
files
|
| Mon, 08 Sep 2008 16:08:23 +0200 |
wenzelm |
moved task, thread_data, group, queue to task_queue.ML;
|
changeset |
files
|
| Mon, 08 Sep 2008 16:08:18 +0200 |
wenzelm |
Ordered queue of grouped tasks.
|
changeset |
files
|
| Mon, 08 Sep 2008 16:08:13 +0200 |
wenzelm |
added Concurrent/task_queue.ML;
|
changeset |
files
|
| Mon, 08 Sep 2008 00:25:34 +0200 |
wenzelm |
await: SYNCHRONIZED wait!
|
changeset |
files
|
| Mon, 08 Sep 2008 00:10:41 +0200 |
wenzelm |
tuned check_cache;
|
changeset |
files
|
| Sun, 07 Sep 2008 22:20:15 +0200 |
wenzelm |
added sync_interrupts, regular_interrupts;
|
changeset |
files
|
| Sun, 07 Sep 2008 22:20:11 +0200 |
wenzelm |
added sync_interrupts, regular_interrupts;
|
changeset |
files
|
| Sun, 07 Sep 2008 22:20:08 +0200 |
wenzelm |
opaque signature constraint abstracts local type abbrev;
|
changeset |
files
|
| Sun, 07 Sep 2008 22:19:58 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 07 Sep 2008 22:19:46 +0200 |
wenzelm |
added change_result;
|
changeset |
files
|
| Sun, 07 Sep 2008 22:19:42 +0200 |
wenzelm |
Functional threads as future values.
|
changeset |
files
|
| Sun, 07 Sep 2008 22:19:31 +0200 |
wenzelm |
added Concurrent/future.ML;
|
changeset |
files
|
| Sun, 07 Sep 2008 17:48:50 +0200 |
wenzelm |
Default (mostly dummy) implementation of thread structures.
|
changeset |
files
|
| Sun, 07 Sep 2008 17:48:49 +0200 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
changeset |
files
|
| Sun, 07 Sep 2008 17:46:44 +0200 |
wenzelm |
*** empty log message ***
|
changeset |
files
|
| Sun, 07 Sep 2008 17:46:43 +0200 |
wenzelm |
explicit use of universal.ML and dummy_thread.ML;
|
changeset |
files
|
| Sun, 07 Sep 2008 17:46:41 +0200 |
wenzelm |
added no_interrupts;
|
changeset |
files
|
| Sun, 07 Sep 2008 17:46:40 +0200 |
wenzelm |
added no_interrupts;
|
changeset |
files
|
| Sun, 07 Sep 2008 17:46:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 07 Sep 2008 17:46:38 +0200 |
wenzelm |
send: broadcast to all waiting threads;
|
changeset |
files
|
| Sun, 07 Sep 2008 17:46:37 +0200 |
wenzelm |
added ML-Systems/thread_dummy.ML;
|
changeset |
files
|
| Sat, 06 Sep 2008 14:02:36 +0200 |
haftmann |
dropped "run" marker in monad syntax
|
changeset |
files
|
| Fri, 05 Sep 2008 11:50:35 +0200 |
wenzelm |
multithreading.ML provides dummy thread structures;
|
changeset |
files
|
| Fri, 05 Sep 2008 06:50:22 +0200 |
haftmann |
different bookkeeping for code equations
|
changeset |
files
|
| Fri, 05 Sep 2008 06:50:20 +0200 |
haftmann |
renamed structure CodeTarget to Code_Target
|
changeset |
files
|
| Fri, 05 Sep 2008 00:19:50 +0200 |
huffman |
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
|
changeset |
files
|
| Thu, 04 Sep 2008 21:12:06 +0200 |
wenzelm |
proper header;
|
changeset |
files
|
| Thu, 04 Sep 2008 21:02:42 +0200 |
wenzelm |
added receive_timeout;
|
changeset |
files
|
| Thu, 04 Sep 2008 20:06:23 +0200 |
wenzelm |
check WRAPPER_OUTPUT node type;
|
changeset |
files
|
| Thu, 04 Sep 2008 20:05:48 +0200 |
wenzelm |
init: disallow "" as out stream;
|
changeset |
files
|
| Thu, 04 Sep 2008 19:47:13 +0200 |
wenzelm |
fixed deps: no Concurrent/receiver.ML yet;
|
changeset |
files
|
| Thu, 04 Sep 2008 19:45:13 +0200 |
wenzelm |
Concurrent message exchange via mailbox -- with unbounded queueing.
|
changeset |
files
|
| Thu, 04 Sep 2008 19:45:12 +0200 |
wenzelm |
added Concurrent/mailbox.ML;
|
changeset |
files
|
| Thu, 04 Sep 2008 17:24:18 +0200 |
huffman |
reorganize subsections
|
changeset |
files
|
| Thu, 04 Sep 2008 17:21:49 +0200 |
huffman |
rename INF_drop_prefix to INFM_drop_prefix
|
changeset |
files
|
| Thu, 04 Sep 2008 17:19:57 +0200 |
huffman |
add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1
|
changeset |
files
|
| Thu, 04 Sep 2008 17:18:44 +0200 |
huffman |
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
|
changeset |
files
|
| Thu, 04 Sep 2008 16:43:51 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Thu, 04 Sep 2008 16:43:50 +0200 |
wenzelm |
added General/queue.ML;
|
changeset |
files
|
| Thu, 04 Sep 2008 16:43:48 +0200 |
wenzelm |
Efficient queues.
|
changeset |
files
|
| Thu, 04 Sep 2008 16:03:49 +0200 |
wenzelm |
moved Multithreading.task/schedule to Concurrent/schedule.ML
|
changeset |
files
|
| Thu, 04 Sep 2008 16:03:48 +0200 |
wenzelm |
multithreading.ML provides dummy thread structures;
|
changeset |
files
|
| Thu, 04 Sep 2008 16:03:47 +0200 |
wenzelm |
moved Multithreading.task/schedule to Concurrent/schedule.ML;
|
changeset |
files
|
| Thu, 04 Sep 2008 16:03:46 +0200 |
wenzelm |
provide dummy thread structures, including proper Thread.getLocal/setLocal;
|
changeset |
files
|
| Thu, 04 Sep 2008 16:03:44 +0200 |
wenzelm |
Thread.getLocal/setLocal;
|
changeset |
files
|
| Thu, 04 Sep 2008 16:03:43 +0200 |
wenzelm |
Scheduling -- multiple threads working on a queue of tasks.
|
changeset |
files
|
| Thu, 04 Sep 2008 16:03:41 +0200 |
wenzelm |
added Concurrent/schedule.ML;
|
changeset |
files
|
| Wed, 03 Sep 2008 20:32:33 +0000 |
convert-repo |
update tags
|
changeset |
files
|
| Wed, 03 Sep 2008 20:04:54 +0200 |
wenzelm |
use /home/isabelle/mercurial/bin/hg wrapper;
|
changeset |
files
|
| Wed, 03 Sep 2008 19:52:45 +0200 |
wenzelm |
exclude large .mov files;
|
changeset |
files
|
| Wed, 03 Sep 2008 17:50:37 +0200 |
wenzelm |
simplified add_axiom: no hyps;
|
changeset |
files
|
| Wed, 03 Sep 2008 17:47:40 +0200 |
wenzelm |
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
|
changeset |
files
|
| Wed, 03 Sep 2008 17:47:38 +0200 |
wenzelm |
axiomatization is now global-only;
|
changeset |
files
|
| Wed, 03 Sep 2008 17:47:37 +0200 |
wenzelm |
added const_decl;
|
changeset |
files
|
| Wed, 03 Sep 2008 17:47:35 +0200 |
wenzelm |
simplified specify_const: canonical args, global deps;
|
changeset |
files
|
| Wed, 03 Sep 2008 17:47:34 +0200 |
wenzelm |
declare_const: Name.binding, store/report position;
|
changeset |
files
|
| Wed, 03 Sep 2008 17:47:30 +0200 |
wenzelm |
Sign.declare_const: Name.binding;
|
changeset |
files
|
| Wed, 03 Sep 2008 12:11:28 +0200 |
nipkow |
removed ex/Puzzle
|
changeset |
files
|
| Wed, 03 Sep 2008 11:44:52 +0200 |
wenzelm |
added qualified: string -> binding -> binding;
|
changeset |
files
|
| Wed, 03 Sep 2008 11:44:48 +0200 |
wenzelm |
Name.qualified;
|
changeset |
files
|
| Wed, 03 Sep 2008 11:27:15 +0200 |
wenzelm |
theorem dependency hook: check previous state;
|
changeset |
files
|
| Wed, 03 Sep 2008 11:26:59 +0200 |
wenzelm |
added pos_of;
|
changeset |
files
|
| Wed, 03 Sep 2008 11:18:55 +0200 |
nipkow |
-> AFP
|
changeset |
files
|
| Wed, 03 Sep 2008 11:09:08 +0200 |
wenzelm |
simplified Toplevel.add_hook: cover successful transactions only;
|
changeset |
files
|
| Wed, 03 Sep 2008 00:11:27 +0200 |
kleing |
retired Ben Porter's DenumRat in favour of the shorter proof in
|
changeset |
files
|
| Tue, 02 Sep 2008 23:52:51 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Tue, 02 Sep 2008 23:27:44 +0200 |
wenzelm |
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
|
changeset |
files
|
| Tue, 02 Sep 2008 22:41:36 +0200 |
wenzelm |
* Generic Toplevel.add_hook interface allows to analyze the result of
|
changeset |
files
|
| Tue, 02 Sep 2008 22:37:20 +0200 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:27 +0200 |
wenzelm |
added new_thms_deps (operates on global facts, some name_hint approximation);
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:25 +0200 |
wenzelm |
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:24 +0200 |
wenzelm |
added add_hook interface for post-transition hooks;
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:21 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:20 +0200 |
wenzelm |
ProofDisplay.print_results;
|
changeset |
files
|
| Tue, 02 Sep 2008 22:20:16 +0200 |
wenzelm |
no pervasive bindings;
|
changeset |
files
|
| Tue, 02 Sep 2008 21:31:28 +0200 |
nipkow |
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
|
changeset |
files
|
| Tue, 02 Sep 2008 20:38:17 +0200 |
haftmann |
distributed literal code generation out of central infrastructure
|
changeset |
files
|
| Tue, 02 Sep 2008 20:07:51 +0200 |
wenzelm |
* Result facts now refer to the *full* internal name;
|
changeset |
files
|
| Tue, 02 Sep 2008 20:04:26 +0200 |
wenzelm |
* Name bindings in higher specification mechanisms;
|
changeset |
files
|
| Tue, 02 Sep 2008 18:01:24 +0200 |
wenzelm |
pretty_fact/results: display base only, since results now come with full names (note that Facts.extern is not really well-defined unless we present the real target context);
|
changeset |
files
|
| Tue, 02 Sep 2008 18:01:23 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 02 Sep 2008 17:31:20 +0200 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
changeset |
files
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:32 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:31 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:30 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:29 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:28 +0200 |
wenzelm |
added binding;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:27 +0200 |
wenzelm |
added fixed_decl, fact_decl, local_fact_decl;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:25 +0200 |
wenzelm |
name_thm etc.: pass position;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:24 +0200 |
wenzelm |
added type binding -- generic name bindings;
|
changeset |
files
|
| Tue, 02 Sep 2008 14:10:19 +0200 |
wenzelm |
name/var morphism operates on Name.binding;
|
changeset |
files
|
| Tue, 02 Sep 2008 12:07:34 +0200 |
haftmann |
adapted to class instantiation compliance
|
changeset |
files
|
| Mon, 01 Sep 2008 22:10:42 +0200 |
nipkow |
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
|
changeset |
files
|
| Mon, 01 Sep 2008 19:17:47 +0200 |
nipkow |
renamed lemma
|
changeset |
files
|
| Mon, 01 Sep 2008 19:17:37 +0200 |
nipkow |
moved more lemmas here from AFP/Integration/Rats
|
changeset |
files
|
| Mon, 01 Sep 2008 19:17:04 +0200 |
nipkow |
moved lemma into SetInterval where it belongs
|
changeset |
files
|
| Mon, 01 Sep 2008 19:16:40 +0200 |
nipkow |
cleaned up code generation for {.._} and {..<_}
|
changeset |
files
|
| Mon, 01 Sep 2008 10:28:04 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Mon, 01 Sep 2008 10:20:14 +0200 |
nipkow |
extended interface to preferences to allow adding new ones
|
changeset |
files
|
| Mon, 01 Sep 2008 10:19:38 +0200 |
nipkow |
Prover is set via menu now
|
changeset |
files
|
| Mon, 01 Sep 2008 10:18:37 +0200 |
haftmann |
restructured code generation of literals
|
changeset |
files
|
| Fri, 29 Aug 2008 20:36:08 +0200 |
wenzelm |
IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
|
changeset |
files
|
| Fri, 29 Aug 2008 20:36:07 +0200 |
wenzelm |
init: more explicit protocol of open/remove rendezvous;
|
changeset |
files
|
| Fri, 29 Aug 2008 20:36:05 +0200 |
wenzelm |
use hardwired /tmp -- fifo only work on local file-system;
|
changeset |
files
|
| Fri, 29 Aug 2008 08:14:59 +0200 |
haftmann |
separate module for code output
|
changeset |
files
|
| Fri, 29 Aug 2008 08:14:58 +0200 |
haftmann |
fixed names of class assumptions
|
changeset |
files
|
| Fri, 29 Aug 2008 07:43:25 +0200 |
haftmann |
dropped parameter prefix for class theorems
|
changeset |
files
|
| Thu, 28 Aug 2008 22:26:23 +0200 |
wenzelm |
added charset (from isabelle_process.scala);
|
changeset |
files
|
| Thu, 28 Aug 2008 22:26:22 +0200 |
wenzelm |
moved charset to isabelle_system.scala;
|
changeset |
files
|
| Thu, 28 Aug 2008 22:26:21 +0200 |
wenzelm |
provide HOME_JVM=HOME to prevent implicit cygpath mangling;
|
changeset |
files
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
changeset |
files
|
| Thu, 28 Aug 2008 22:08:11 +0200 |
haftmann |
no parameter prefix for class interpretation
|
changeset |
files
|
| Thu, 28 Aug 2008 22:08:02 +0200 |
haftmann |
updated
|
changeset |
files
|
| Thu, 28 Aug 2008 20:29:40 +0200 |
wenzelm |
tuned fold_lines;
|
changeset |
files
|
| Thu, 28 Aug 2008 20:19:45 +0200 |
wenzelm |
fold_lines: simplified, more efficient due to String.fields;
|
changeset |
files
|
| Thu, 28 Aug 2008 19:34:51 +0200 |
wenzelm |
rm fifo after open;
|
changeset |
files
|
| Thu, 28 Aug 2008 19:31:55 +0200 |
wenzelm |
dummy setup for completion;
|
changeset |
files
|
| Thu, 28 Aug 2008 19:31:13 +0200 |
wenzelm |
create named pipe;
|
changeset |
files
|
| Thu, 28 Aug 2008 19:29:59 +0200 |
wenzelm |
added is_cygwin;
|
changeset |
files
|
| Thu, 28 Aug 2008 19:29:58 +0200 |
wenzelm |
join stdout/stderr, eliminated Kind.STDERR;
|
changeset |
files
|
| Thu, 28 Aug 2008 19:29:57 +0200 |
wenzelm |
explicit output stream, typically a named pipe;
|
changeset |
files
|
| Thu, 28 Aug 2008 19:29:56 +0200 |
wenzelm |
refined option -W: output stream;
|
changeset |
files
|
| Thu, 28 Aug 2008 17:54:18 +0200 |
krauss |
more function -> fun
|
changeset |
files
|
| Thu, 28 Aug 2008 15:33:33 +0200 |
krauss |
quicksort: function -> fun
|
changeset |
files
|
| Thu, 28 Aug 2008 15:24:30 +0200 |
krauss |
corrected some typos
|
changeset |
files
|
| Thu, 28 Aug 2008 00:49:54 +0200 |
wenzelm |
fixed atom_to_xml: literal "name" attribute;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:19 +0200 |
wenzelm |
exported atom_to_xml;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:17 +0200 |
wenzelm |
changed Markup print mode to YXML -- explicitly decode messages before being issued;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:15 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:13 +0200 |
wenzelm |
present_token: disable print_mode, which is YXML now;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:11 +0200 |
wenzelm |
text_of Malformed: explode with spaces -- Output.output/escape ineffective by default;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:09 +0200 |
wenzelm |
removed obsolete XML.Output workaround;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:08 +0200 |
wenzelm |
added get_int;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:07 +0200 |
wenzelm |
removed obsolete get_string;
|
changeset |
files
|
| Thu, 28 Aug 2008 00:33:04 +0200 |
wenzelm |
removed obsolete ProofGeneral/pgml_isabelle.ML;
|
changeset |
files
|
| Wed, 27 Aug 2008 23:46:33 +0200 |
huffman |
simplify definition of vector_space locale (use axclasses instead of inheriting from field and ab_group_add classes)
|
changeset |
files
|
| Wed, 27 Aug 2008 20:36:27 +0200 |
wenzelm |
renamed Buffer.write to File.write_buffer;
|
changeset |
files
|
| Wed, 27 Aug 2008 20:36:26 +0200 |
wenzelm |
renamed Buffer.write to File.write_buffer;
|
changeset |
files
|
| Wed, 27 Aug 2008 20:36:25 +0200 |
wenzelm |
load buffer.ML before file.ML;
|
changeset |
files
|
| Wed, 27 Aug 2008 20:36:23 +0200 |
wenzelm |
replaced find_substring by first_field;
|
changeset |
files
|
| Wed, 27 Aug 2008 17:54:31 +0200 |
ballarin |
Consistent naming of theorems in interpretation.
|
changeset |
files
|
| Wed, 27 Aug 2008 16:32:48 +0200 |
wenzelm |
simplified parse_attrib (find_substring instead of space_explode);
|
changeset |
files
|
| Wed, 27 Aug 2008 16:32:18 +0200 |
wenzelm |
added find_substring;
|
changeset |
files
|
| Wed, 27 Aug 2008 12:01:59 +0200 |
haftmann |
added HOL/ex/Numeral.thy
|
changeset |
files
|
| Wed, 27 Aug 2008 12:00:28 +0200 |
wenzelm |
get rid of tabs;
|
changeset |
files
|
| Wed, 27 Aug 2008 11:49:50 +0200 |
wenzelm |
Property lists.
|
changeset |
files
|
| Wed, 27 Aug 2008 11:49:14 +0200 |
wenzelm |
added General/properties.ML;
|
changeset |
files
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:35 +0200 |
haftmann |
proper error message
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:34 +0200 |
haftmann |
proper handling of type variabl names
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:32 +0200 |
haftmann |
completing arities after subclass instance
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:31 +0200 |
haftmann |
untabification
|
changeset |
files
|
| Wed, 27 Aug 2008 11:24:29 +0200 |
haftmann |
tuned code generator setup
|
changeset |
files
|
| Wed, 27 Aug 2008 04:47:30 +0200 |
urbanc |
added equivariance lemmas for ex1 and the
|
changeset |
files
|
| Wed, 27 Aug 2008 01:27:33 +0200 |
huffman |
add lemmas about Rats similar to those about Reals
|
changeset |
files
|
| Tue, 26 Aug 2008 23:49:46 +0200 |
huffman |
move real_vector class proofs into vector_space and group_hom locales
|
changeset |
files
|
| Tue, 26 Aug 2008 18:59:52 +0200 |
krauss |
added distributivity of relation composition over union [simp]
|
changeset |
files
|
| Tue, 26 Aug 2008 16:36:30 +0200 |
wenzelm |
tuned append;
|
changeset |
files
|
| Tue, 26 Aug 2008 16:36:11 +0200 |
wenzelm |
command: symbols.encode;
|
changeset |
files
|
| Tue, 26 Aug 2008 16:04:22 +0200 |
ballarin |
Reorganisation of registration code.
|
changeset |
files
|
| Tue, 26 Aug 2008 14:15:44 +0200 |
krauss |
function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes
|
changeset |
files
|
| Tue, 26 Aug 2008 12:20:52 +0200 |
wenzelm |
purge classes after compilation;
|
changeset |
files
|
| Tue, 26 Aug 2008 12:17:58 +0200 |
wenzelm |
renamed Isabelle-repository to isabelle;
|
changeset |
files
|
| Tue, 26 Aug 2008 12:07:06 +0200 |
nipkow |
Defined rationals (Rats) globally in Rational.
|
changeset |
files
|
| Tue, 26 Aug 2008 11:42:46 +0200 |
wenzelm |
replaced /home/isabelle/html-data/isabelle-repos by /home/isabelle-repository/repos;
|
changeset |
files
|
| Mon, 25 Aug 2008 23:27:56 +0200 |
wenzelm |
moved new Symbol.Interpretation into plugin;
|
changeset |
files
|
| Mon, 25 Aug 2008 22:42:04 +0200 |
wenzelm |
promoted to EBPlugin;
|
changeset |
files
|
| Mon, 25 Aug 2008 22:26:26 +0200 |
wenzelm |
explicitly depend on isabelle-Pure.jar and isabelle-scala-library.jar;
|
changeset |
files
|
| Mon, 25 Aug 2008 22:05:30 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 25 Aug 2008 21:59:36 +0200 |
wenzelm |
isabelle process: pick options/args from properties;
|
changeset |
files
|
| Mon, 25 Aug 2008 21:58:54 +0200 |
wenzelm |
removed unused ConsolePlugin dependency;
|
changeset |
files
|
| Mon, 25 Aug 2008 20:01:17 +0200 |
wenzelm |
simplified exceptions: use plain error function / RuntimeException;
|
changeset |
files
|
| Mon, 25 Aug 2008 16:52:11 +0200 |
wenzelm |
added try_result;
|
changeset |
files
|
| Sun, 24 Aug 2008 21:15:48 +0200 |
wenzelm |
misc reorganization;
|
changeset |
files
|
| Sun, 24 Aug 2008 21:15:46 +0200 |
wenzelm |
Kind: added is_control;
|
changeset |
files
|
| Sun, 24 Aug 2008 21:15:44 +0200 |
wenzelm |
get: allow null;
|
changeset |
files
|
| Sun, 24 Aug 2008 19:24:27 +0200 |
wenzelm |
misc tuning of names;
|
changeset |
files
|
| Sun, 24 Aug 2008 19:02:22 +0200 |
wenzelm |
rearranged source files;
|
changeset |
files
|
| Sun, 24 Aug 2008 18:57:43 +0200 |
wenzelm |
init_message: class markup in message body, not header;
|
changeset |
files
|
| Sun, 24 Aug 2008 18:11:20 +0200 |
wenzelm |
repackaged as isabelle.jedit;
|
changeset |
files
|
| Sun, 24 Aug 2008 17:23:42 +0200 |
wenzelm |
untabify: silently turn tab into space if column information is unavailable;
|
changeset |
files
|
| Sun, 24 Aug 2008 14:42:26 +0200 |
haftmann |
corrected cache handling for class operations
|
changeset |
files
|
| Sun, 24 Aug 2008 14:42:24 +0200 |
haftmann |
default replaces arbitrary
|
changeset |
files
|
| Sun, 24 Aug 2008 14:42:22 +0200 |
haftmann |
tuned import order
|
changeset |
files
|
| Sun, 24 Aug 2008 14:24:03 +0200 |
wenzelm |
activated \<A>, \<a>, \<AA>, \<aa>;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:44:31 +0200 |
wenzelm |
* Isabelle/lib/classes/Pure.jar;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:24:16 +0200 |
wenzelm |
jars: removed obsolete Java process wrapper (cf. new Pure.jar);
|
changeset |
files
|
| Sat, 23 Aug 2008 23:21:50 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:20:43 +0200 |
wenzelm |
obsolete -- superceded by Pure.jar (Scala version);
|
changeset |
files
|
| Sat, 23 Aug 2008 23:17:11 +0200 |
wenzelm |
updated to Pure.jar;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:46 +0200 |
wenzelm |
added exec;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:44 +0200 |
wenzelm |
moved class Result into static object, removed dynamic tree method;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:43 +0200 |
wenzelm |
symbolic message markup;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:41 +0200 |
wenzelm |
renamed Markup.MALFORMED to Markup.BAD;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:39 +0200 |
wenzelm |
added position, messages;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:38 +0200 |
wenzelm |
added messages and process information;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:36 +0200 |
wenzelm |
Position properties.
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:34 +0200 |
wenzelm |
added General/position.scala;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:30 +0200 |
wenzelm |
adapted to new IsabelleProcess from Pure.jar;
|
changeset |
files
|
| Sat, 23 Aug 2008 23:07:28 +0200 |
wenzelm |
include ../../classes/Pure.jar;
|
changeset |
files
|
| Sat, 23 Aug 2008 21:06:32 +0200 |
nipkow |
added const Rational
|
changeset |
files
|
| Sat, 23 Aug 2008 19:42:17 +0200 |
wenzelm |
YXML.parse_failsafe;
|
changeset |
files
|
| Sat, 23 Aug 2008 19:42:16 +0200 |
wenzelm |
shell_prefix: physical /bin/env on Cygwin;
|
changeset |
files
|
| Sat, 23 Aug 2008 19:42:15 +0200 |
wenzelm |
removed full_markup mode (default);
|
changeset |
files
|
| Sat, 23 Aug 2008 19:42:14 +0200 |
wenzelm |
added parse_failsafe;
|
changeset |
files
|
| Sat, 23 Aug 2008 19:42:13 +0200 |
wenzelm |
refer to symbolic Markup;
|
changeset |
files
|
| Sat, 23 Aug 2008 19:42:12 +0200 |
wenzelm |
Common markup elements.
|
changeset |
files
|
| Sat, 23 Aug 2008 19:42:11 +0200 |
wenzelm |
added General/markup.scala;
|
changeset |
files
|
| Sat, 23 Aug 2008 17:55:27 +0200 |
wenzelm |
BadVariable: toString;
|
changeset |
files
|
| Sat, 23 Aug 2008 17:55:26 +0200 |
wenzelm |
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
|
changeset |
files
|
| Sat, 23 Aug 2008 17:55:26 +0200 |
wenzelm |
append_string: proper backslash in character escapes;
|
changeset |
files
|
| Sat, 23 Aug 2008 17:22:54 +0200 |
wenzelm |
added getenv;
|
changeset |
files
|
| Sat, 23 Aug 2008 17:22:53 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 23 Aug 2008 17:22:52 +0200 |
wenzelm |
Isabelle outer syntax.
|
changeset |
files
|
| Sat, 23 Aug 2008 17:22:51 +0200 |
wenzelm |
added Tools/isabelle_process.scala, Tools/isabelle_syntax.scala;
|
changeset |
files
|
| Sat, 23 Aug 2008 17:22:51 +0200 |
wenzelm |
Isabelle process management -- always reactive due to multi-threaded I/O.
|
changeset |
files
|
| Sat, 23 Aug 2008 11:48:52 +0200 |
wenzelm |
renamed DOM to document, add xml version and optional stylesheets;
|
changeset |
files
|
| Fri, 22 Aug 2008 21:25:19 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Thu, 21 Aug 2008 22:06:17 +0200 |
wenzelm |
parse_attrib: proper index of name end!
|
changeset |
files
|
| Thu, 21 Aug 2008 21:42:16 +0200 |
wenzelm |
tuned parse performance: avoid splitting terminal Y chunk;
|
changeset |
files
|
| Thu, 21 Aug 2008 21:27:07 +0200 |
wenzelm |
parse_attrib: more efficient due to indexOf('=');
|
changeset |
files
|
| Thu, 21 Aug 2008 20:53:31 +0200 |
wenzelm |
replaced Pattern.split by chunks iterator (more efficient, resembles ML version more closely);
|
changeset |
files
|
| Thu, 21 Aug 2008 20:51:41 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Thu, 21 Aug 2008 19:19:31 +0200 |
wenzelm |
added iterator over content;
|
changeset |
files
|
| Thu, 21 Aug 2008 17:42:59 +0200 |
wenzelm |
proper ISABELLE_ROOT_JVM on Cygwin;
|
changeset |
files
|
| Thu, 21 Aug 2008 16:02:54 +0200 |
wenzelm |
pattern: proper "." not "[.]"!
|
changeset |
files
|
| Thu, 21 Aug 2008 15:27:28 +0200 |
wenzelm |
recode: proper result for unmatched symbols;
|
changeset |
files
|
| Thu, 21 Aug 2008 15:20:00 +0200 |
wenzelm |
more robust pattern: look at longer matches first, added catch-all case;
|
changeset |
files
|
| Thu, 21 Aug 2008 13:05:37 +0200 |
wenzelm |
added get_setting;
|
changeset |
files
|
| Thu, 21 Aug 2008 13:05:31 +0200 |
wenzelm |
read_symbols: proper IsabelleSystem.platform_path;
|
changeset |
files
|
| Thu, 21 Aug 2008 13:05:28 +0200 |
wenzelm |
added ISABELLE_ROOT_JVM;
|
changeset |
files
|
| Mon, 18 Aug 2008 17:57:06 +0200 |
ballarin |
Theorem on polynomial division and lemmas.
|
changeset |
files
|
| Sun, 17 Aug 2008 21:11:24 +0200 |
wenzelm |
removed parse_element -- no longer fits to liberal parse!
|
changeset |
files
|
| Sun, 17 Aug 2008 21:11:08 +0200 |
wenzelm |
Minimalistic XML tree values.
|
changeset |
files
|
| Sun, 17 Aug 2008 21:11:06 +0200 |
wenzelm |
Efficient text representation of XML trees.
|
changeset |
files
|
| Sun, 17 Aug 2008 21:11:04 +0200 |
wenzelm |
added General/xml.scala, General/yxml.scala;
|
changeset |
files
|
| Sun, 17 Aug 2008 16:45:19 +0200 |
wenzelm |
decode escaped symbols as well;
|
changeset |
files
|
| Sat, 16 Aug 2008 23:51:09 +0200 |
wenzelm |
tuned Recoder;
|
changeset |
files
|
| Sat, 16 Aug 2008 23:29:02 +0200 |
wenzelm |
more private fields;
|
changeset |
files
|
| Sat, 16 Aug 2008 23:28:38 +0200 |
wenzelm |
jar: invoke scaladoc;
|
changeset |
files
|
| Sat, 16 Aug 2008 23:12:23 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 16 Aug 2008 21:23:03 +0200 |
wenzelm |
use scala.collection.jcl.HashMap, which seems to be more efficient;
|
changeset |
files
|
| Sat, 16 Aug 2008 21:23:01 +0200 |
wenzelm |
jar target: removed jvmpath -- does not work on Linux!?
|
changeset |
files
|
| Sat, 16 Aug 2008 16:44:10 +0200 |
wenzelm |
add scala-library.jar if available;
|
changeset |
files
|
| Sat, 16 Aug 2008 16:43:03 +0200 |
wenzelm |
jar target: jvmpath;
|
changeset |
files
|
| Sat, 16 Aug 2008 16:01:53 +0200 |
wenzelm |
Isabelle system support.
|
changeset |
files
|
| Sat, 16 Aug 2008 15:57:06 +0200 |
wenzelm |
reading symbol interpretation tables;
|
changeset |
files
|
| Sat, 16 Aug 2008 15:57:05 +0200 |
wenzelm |
added Tools/isabelle_system.scala;
|
changeset |
files
|
| Sat, 16 Aug 2008 14:29:25 +0200 |
wenzelm |
removed unused usage;
|
changeset |
files
|
| Sat, 16 Aug 2008 13:32:23 +0200 |
wenzelm |
more robust handling of directory layout variants;
|
changeset |
files
|
| Sat, 16 Aug 2008 13:31:57 +0200 |
wenzelm |
refined scala/java wrappers via isatool;
|
changeset |
files
|
| Sat, 16 Aug 2008 13:31:56 +0200 |
wenzelm |
tuned abbrevs;
|
changeset |
files
|
| Sat, 16 Aug 2008 13:31:55 +0200 |
wenzelm |
added ISABELLE_SCALA, ISABELLE_JAVA;
|
changeset |
files
|
| Fri, 15 Aug 2008 23:31:37 +0200 |
wenzelm |
added ISABELLE_HOME_JVM;
|
changeset |
files
|
| Fri, 15 Aug 2008 23:10:36 +0200 |
wenzelm |
proper jvmpath for cygwin;
|
changeset |
files
|
| Fri, 15 Aug 2008 23:09:55 +0200 |
wenzelm |
proper RC;
|
changeset |
files
|
| Fri, 15 Aug 2008 22:59:02 +0200 |
wenzelm |
refined JVM path wrappers: Isabelle environment holds Unix version of CLASSPATH, javawrapper/scalawrapper convert it back;
|
changeset |
files
|
| Fri, 15 Aug 2008 22:59:01 +0200 |
wenzelm |
refined JVM path wrappers;
|
changeset |
files
|
| Fri, 15 Aug 2008 22:58:59 +0200 |
wenzelm |
added JVM components (Scala or Java);
|
changeset |
files
|
| Fri, 15 Aug 2008 22:16:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 15 Aug 2008 22:16:13 +0200 |
wenzelm |
jars: build Pure.jar;
|
changeset |
files
|
| Fri, 15 Aug 2008 21:57:22 +0200 |
wenzelm |
scan: proper recovery for escaped \\< symbols;
|
changeset |
files
|
| Fri, 15 Aug 2008 21:56:07 +0200 |
wenzelm |
basic setup for Scala material;
|
changeset |
files
|
| Fri, 15 Aug 2008 21:53:40 +0200 |
wenzelm |
Basic support for Isabelle symbols.
|
changeset |
files
|
| Fri, 15 Aug 2008 18:25:41 +0200 |
wenzelm |
added some abbrevs;
|
changeset |
files
|
| Fri, 15 Aug 2008 18:03:30 +0200 |
wenzelm |
removed redundant "symbol" property;
|
changeset |
files
|
| Fri, 15 Aug 2008 17:19:32 +0200 |
wenzelm |
Default interpretation of some Isabelle symbols.
|
changeset |
files
|
| Fri, 15 Aug 2008 17:03:58 +0200 |
wenzelm |
report antiquotation names;
|
changeset |
files
|
| Fri, 15 Aug 2008 17:03:56 +0200 |
wenzelm |
fixed DOCTYPE -- XHTML is case-sensitive!
|
changeset |
files
|
| Fri, 15 Aug 2008 17:03:55 +0200 |
wenzelm |
report antiquotation names;
|
changeset |
files
|
| Fri, 15 Aug 2008 17:03:52 +0200 |
wenzelm |
added ML_antiq, doc_antiq;
|
changeset |
files
|
| Fri, 15 Aug 2008 16:08:08 +0200 |
wenzelm |
added README;
|
changeset |
files
|
| Fri, 15 Aug 2008 16:06:01 +0200 |
wenzelm |
generated truetype font;
|
changeset |
files
|
| Fri, 15 Aug 2008 16:04:57 +0200 |
wenzelm |
The Jerusalem font from 2004 -- unicode version.
|
changeset |
files
|
| Fri, 15 Aug 2008 15:51:06 +0200 |
wenzelm |
args: explicit groups for file_name, theory_name;
|
changeset |
files
|
| Fri, 15 Aug 2008 15:51:04 +0200 |
wenzelm |
read_asts: Lexicon.report_token, filter Lexicon.is_proper;
|
changeset |
files
|
| Fri, 15 Aug 2008 15:51:02 +0200 |
wenzelm |
filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;
|
changeset |
files
|
| Fri, 15 Aug 2008 15:51:00 +0200 |
wenzelm |
token_kind: add Space, Comment;
|
changeset |
files
|
| Fri, 15 Aug 2008 15:50:58 +0200 |
wenzelm |
renamed T.source_of' to T.source_position_of;
|
changeset |
files
|
| Fri, 15 Aug 2008 15:50:52 +0200 |
wenzelm |
renamed T.source_of' to T.source_position_of;
|
changeset |
files
|
| Fri, 15 Aug 2008 15:50:50 +0200 |
wenzelm |
output_markup: check Markup.is_none;
|
changeset |
files
|
| Fri, 15 Aug 2008 15:50:49 +0200 |
wenzelm |
added is_none;
|
changeset |
files
|
| Fri, 15 Aug 2008 15:50:44 +0200 |
wenzelm |
Args.name_source(_position) for proper position information;
|
changeset |
files
|
| Thu, 14 Aug 2008 21:06:07 +0200 |
wenzelm |
[source=false] for quoted antiquotation avoids quote-escapes in output;
|
changeset |
files
|
| Thu, 14 Aug 2008 20:29:38 +0200 |
wenzelm |
report antiquotations;
|
changeset |
files
|
| Thu, 14 Aug 2008 20:29:37 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 14 Aug 2008 20:13:43 +0200 |
wenzelm |
report ML_source;
|
changeset |
files
|
| Thu, 14 Aug 2008 20:13:42 +0200 |
wenzelm |
renamed P.ml_source to P.ML_source;
|
changeset |
files
|
| Thu, 14 Aug 2008 20:13:41 +0200 |
wenzelm |
report doc_source;
|
changeset |
files
|
| Thu, 14 Aug 2008 20:13:40 +0200 |
wenzelm |
added ML_source, doc_source;
|
changeset |
files
|
| Thu, 14 Aug 2008 19:52:40 +0200 |
wenzelm |
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
|
changeset |
files
|
| Thu, 14 Aug 2008 19:52:39 +0200 |
wenzelm |
added source_of';
|
changeset |
files
|
| Thu, 14 Aug 2008 19:52:37 +0200 |
wenzelm |
P.doc_source and P.ml_sorce for proper SymbolPos.text;
|
changeset |
files
|
| Thu, 14 Aug 2008 19:52:36 +0200 |
wenzelm |
oracle, header/local_theory/proof_markup: pass SymbolPos.text;
|
changeset |
files
|
| Thu, 14 Aug 2008 19:52:35 +0200 |
wenzelm |
use SymbolPos.T list directly, instead of encoded SymbolPos.text;
|
changeset |
files
|
| Thu, 14 Aug 2008 16:52:56 +0200 |
wenzelm |
ML_Context.add_antiq: pass position;
|
changeset |
files
|
| Thu, 14 Aug 2008 16:52:54 +0200 |
wenzelm |
ML_Context.add_antiq: pass position;
|
changeset |
files
|
| Thu, 14 Aug 2008 16:52:52 +0200 |
wenzelm |
retrieve_thms: transfer fact position to result;
|
changeset |
files
|
| Thu, 14 Aug 2008 16:52:51 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm;
|
changeset |
files
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
changeset |
files
|
| Thu, 14 Aug 2008 11:55:05 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:40 +0200 |
wenzelm |
removed obsolete present_html -- now part of regular theory presentation;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:39 +0200 |
wenzelm |
removed obsolete verbatim_source, results, chapter, section etc.;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:37 +0200 |
wenzelm |
removed obsolete verbatim_source, results, chapter, section etc.;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:35 +0200 |
wenzelm |
ProofDisplay.add_hook;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:33 +0200 |
wenzelm |
simplified present_local_theory/proof;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:33 +0200 |
wenzelm |
ProofDisplay.theory_results;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:31 +0200 |
wenzelm |
removed obsolete present_results;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:30 +0200 |
wenzelm |
scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:30 +0200 |
wenzelm |
load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:28 +0200 |
wenzelm |
simplified markup commands;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:26 +0200 |
wenzelm |
simplified markup commands -- removed obsolete Present.results, always check text;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:24 +0200 |
wenzelm |
added untabify_content;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:22 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:20 +0200 |
wenzelm |
removed obsolete untabify (superceded by SymbolPos.tabify_content);
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:18 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Wed, 13 Aug 2008 20:57:16 +0200 |
wenzelm |
removed obsolete theorems;
|
changeset |
files
|
| Wed, 13 Aug 2008 03:00:33 +0200 |
berghofe |
Changed proof of strong induction rule to avoid infinite loop
|
changeset |
files
|
| Tue, 12 Aug 2008 21:48:59 +0200 |
wenzelm |
token_kind_markup: complete coverage;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:28:09 +0200 |
wenzelm |
OuterSyntax.scan: pass position;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:28:07 +0200 |
wenzelm |
message: ignored if body empty;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:28:05 +0200 |
wenzelm |
load_thy: removed obsolete dir argument;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:28:03 +0200 |
wenzelm |
abstract type span, tuned interfaces;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:28:01 +0200 |
wenzelm |
adapted ThyEdit operations;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:27:59 +0200 |
wenzelm |
added ignored, malformed transitions;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:27:57 +0200 |
wenzelm |
Symbol.source/OuterLex.source: more explicit do_recover argument;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:27:55 +0200 |
wenzelm |
Isabelle.command: inline former OuterSyntax.prepare_command;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:27:53 +0200 |
wenzelm |
load thy_edit.ML before outer_syntax.ML;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:27:51 +0200 |
wenzelm |
renamed unknown_span to malformed_span;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:27:48 +0200 |
wenzelm |
Symbol.source/OuterLex.source: more explicit do_recover argument;
|
changeset |
files
|
| Tue, 12 Aug 2008 21:27:46 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Mon, 11 Aug 2008 22:25:45 +0200 |
haftmann |
rudimentary code setup for set operations
|
changeset |
files
|
| Mon, 11 Aug 2008 22:06:51 +0200 |
wenzelm |
<applet>: more XHTML 1.0 Transitional conformance;
|
changeset |
files
|
| Mon, 11 Aug 2008 22:06:49 +0200 |
wenzelm |
Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;
|
changeset |
files
|
| Mon, 11 Aug 2008 20:56:32 +0200 |
wenzelm |
<pre>: removed xml:space, is already default;
|
changeset |
files
|
| Mon, 11 Aug 2008 18:37:51 +0200 |
wenzelm |
produce XHTML 1.0 Transitional;
|
changeset |
files
|
| Mon, 11 Aug 2008 18:37:49 +0200 |
wenzelm |
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
|
changeset |
files
|
| Mon, 11 Aug 2008 17:37:48 +0200 |
wenzelm |
Isar.command: do not set position of enclosing transaction, to avoid of clash with the one being prepared here!
|
changeset |
files
|
| Mon, 11 Aug 2008 14:50:04 +0200 |
haftmann |
changed code setup
|
changeset |
files
|
| Mon, 11 Aug 2008 14:50:02 +0200 |
haftmann |
re-arranged class dense_linear_order
|
changeset |
files
|
| Mon, 11 Aug 2008 14:50:00 +0200 |
haftmann |
rudimentary code setup for set operations
|
changeset |
files
|
| Mon, 11 Aug 2008 14:49:53 +0200 |
haftmann |
moved class wellorder to theory Orderings
|
changeset |
files
|
| Sun, 10 Aug 2008 12:38:26 +0200 |
wenzelm |
added parse_token (from proof_context.ML);
|
changeset |
files
|
| Sun, 10 Aug 2008 12:38:25 +0200 |
wenzelm |
read_tyname/const/const_proper: report position;
|
changeset |
files
|
| Sun, 10 Aug 2008 12:38:24 +0200 |
wenzelm |
pass position to get_fact;
|
changeset |
files
|
| Sun, 10 Aug 2008 12:38:23 +0200 |
wenzelm |
pass token source to typ/term etc.;
|
changeset |
files
|
| Sun, 10 Aug 2008 12:38:22 +0200 |
wenzelm |
added name property operation;
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:59 +0200 |
wenzelm |
renamed ML_Lex.val_of to content_of;
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:58 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:57 +0200 |
wenzelm |
unified Args.T with OuterLex.token;
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:56 +0200 |
wenzelm |
unified Args.T with OuterLex.token;
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:55 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:54 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:53 +0200 |
wenzelm |
unified Args.T with OuterLex.token;
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:52 +0200 |
wenzelm |
load args.ML later (after outer_parse.ML);
|
changeset |
files
|
| Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
changeset |
files
|
| Sat, 09 Aug 2008 12:28:13 +0200 |
wenzelm |
read_asts: report literal tokens;
|
changeset |
files
|
| Sat, 09 Aug 2008 12:28:12 +0200 |
wenzelm |
tuned error message;
|
changeset |
files
|
| Sat, 09 Aug 2008 12:28:11 +0200 |
wenzelm |
pos_of_token: Position.T;
|
changeset |
files
|
| Sat, 09 Aug 2008 12:28:10 +0200 |
wenzelm |
dest: sort strings;
|
changeset |
files
|
| Sat, 09 Aug 2008 12:28:09 +0200 |
wenzelm |
added literal;
|
changeset |
files
|
| Sat, 09 Aug 2008 00:09:39 +0200 |
wenzelm |
read_token: more robust handling of empty text;
|
changeset |
files
|
| Sat, 09 Aug 2008 00:09:38 +0200 |
wenzelm |
datatype token: maintain range, tuned representation;
|
changeset |
files
|
| Sat, 09 Aug 2008 00:09:36 +0200 |
wenzelm |
datatype token: maintain range, tuned representation;
|
changeset |
files
|
| Sat, 09 Aug 2008 00:09:35 +0200 |
wenzelm |
datatype token: maintain range, tuned representation;
|
changeset |
files
|
| Sat, 09 Aug 2008 00:09:34 +0200 |
wenzelm |
tuned SymbolPos interface;
|
changeset |
files
|
| Sat, 09 Aug 2008 00:09:31 +0200 |
wenzelm |
YXML.parse: allow text without markup, potentially empty;
|
changeset |
files
|
| Sat, 09 Aug 2008 00:09:29 +0200 |
wenzelm |
added content;
|
changeset |
files
|
| Sat, 09 Aug 2008 00:09:26 +0200 |
wenzelm |
added distance_of (permissive version);
|
changeset |
files
|
| Fri, 08 Aug 2008 19:29:01 +0200 |
wenzelm |
count offset as well;
|
changeset |
files
|
| Fri, 08 Aug 2008 19:28:59 +0200 |
wenzelm |
added offset/end_offset;
|
changeset |
files
|
| Fri, 08 Aug 2008 16:54:33 +0200 |
wenzelm |
tuned formatting;
|
changeset |
files
|
| Fri, 08 Aug 2008 15:36:40 +0200 |
krauss |
clean up dead code
|
changeset |
files
|
| Fri, 08 Aug 2008 13:36:44 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 08 Aug 2008 09:44:16 +0200 |
krauss |
FundefLib.try_proof : attempt a proof and see if it works
|
changeset |
files
|
| Fri, 08 Aug 2008 09:26:15 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Thu, 07 Aug 2008 23:56:45 +0200 |
wenzelm |
inner_syntax markup is back;
|
changeset |
files
|
| Thu, 07 Aug 2008 23:32:49 +0200 |
wenzelm |
disabled inner_syntax markup for now;
|
changeset |
files
|
| Thu, 07 Aug 2008 22:32:03 +0200 |
wenzelm |
added read_token -- with optional YXML encoding of position;
|
changeset |
files
|
| Thu, 07 Aug 2008 22:32:01 +0200 |
wenzelm |
parse_token: use Syntax.read_token, pass full position information;
|
changeset |
files
|
| Thu, 07 Aug 2008 21:13:01 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 07 Aug 2008 21:07:57 +0200 |
wenzelm |
map_default: more explicit scope;
|
changeset |
files
|
| Thu, 07 Aug 2008 21:07:55 +0200 |
wenzelm |
datatype lexicon: alternative representation using nested Symtab.table;
|
changeset |
files
|
| Thu, 07 Aug 2008 19:21:43 +0200 |
wenzelm |
simplified Antiquote signature;
|
changeset |
files
|
| Thu, 07 Aug 2008 19:21:42 +0200 |
wenzelm |
more precise positions due to SymbolsPos.implode_delim;
|
changeset |
files
|
| Thu, 07 Aug 2008 19:21:41 +0200 |
wenzelm |
simplified Antiq: regular SymbolPos.text with position;
|
changeset |
files
|
| Thu, 07 Aug 2008 19:21:40 +0200 |
wenzelm |
renamed SymbolPos.scan_position to SymbolPos.scan_pos;
|
changeset |
files
|
| Thu, 07 Aug 2008 19:21:39 +0200 |
wenzelm |
only increment column if valid;
|
changeset |
files
|
| Thu, 07 Aug 2008 19:21:38 +0200 |
wenzelm |
install_pp Position.T;
|
changeset |
files
|
| Thu, 07 Aug 2008 19:21:37 +0200 |
wenzelm |
Position.start;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:45:15 +0200 |
wenzelm |
SymbolPos.explode;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:45:13 +0200 |
wenzelm |
improved position handling due to SymbolPos.T;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:45:11 +0200 |
wenzelm |
improved position handling due to SymbolPos.T;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:45:09 +0200 |
wenzelm |
Antiquote.read/read_arguments;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:45:07 +0200 |
wenzelm |
updated type of nested sources;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:45:05 +0200 |
wenzelm |
improved position handling due to SymbolPos.T;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:45:03 +0200 |
wenzelm |
adapted Scan.extend_lexicon/merge_lexicons;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:44:56 +0200 |
wenzelm |
renamed scan_antiquotes to read;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:44:52 +0200 |
wenzelm |
export not_eof;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:44:47 +0200 |
wenzelm |
reorganized lexicon: allow scanning of annotated symbols, tuned representation and interfaces;
|
changeset |
files
|
| Thu, 07 Aug 2008 13:44:42 +0200 |
wenzelm |
advance: single argument (again);
|
changeset |
files
|
| Thu, 07 Aug 2008 13:44:36 +0200 |
wenzelm |
Symbols with explicit position information.
|
changeset |
files
|
| Thu, 07 Aug 2008 13:44:33 +0200 |
wenzelm |
added General/symbol_pos.ML;
|
changeset |
files
|
| Wed, 06 Aug 2008 16:41:40 +0200 |
ballarin |
Interpretation command (theory/proof context) no longer simplifies goal.
|
changeset |
files
|
| Wed, 06 Aug 2008 13:57:25 +0200 |
nipkow |
added lemma
|
changeset |
files
|
| Wed, 06 Aug 2008 10:43:42 +0200 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Wed, 06 Aug 2008 00:58:27 +0200 |
berghofe |
Reverted last change, since it caused incompatibilities.
|
changeset |
files
|
| Wed, 06 Aug 2008 00:12:31 +0200 |
wenzelm |
fall back on P.term_group, to avoid problems with inner_syntax markup (due to CodeName.read_const_exprs);
|
changeset |
files
|
| Wed, 06 Aug 2008 00:12:26 +0200 |
wenzelm |
T.end_position_of;
|
changeset |
files
|
| Wed, 06 Aug 2008 00:12:21 +0200 |
wenzelm |
adapted Antiq;
|
changeset |
files
|
| Wed, 06 Aug 2008 00:12:02 +0200 |
wenzelm |
parse_sort/typ/term/prop: report markup;
|
changeset |
files
|
| Wed, 06 Aug 2008 00:11:12 +0200 |
wenzelm |
sort/typ/term/prop: inner_syntax markup encodes original source position;
|
changeset |
files
|
| Wed, 06 Aug 2008 00:10:31 +0200 |
wenzelm |
removed obsolete range_of (already included in position);
|
changeset |
files
|
| Wed, 06 Aug 2008 00:10:22 +0200 |
wenzelm |
report markup;
|
changeset |
files
|
| Wed, 06 Aug 2008 00:10:18 +0200 |
wenzelm |
Antiq: inner vs. outer position;
|
changeset |
files
|
| Wed, 06 Aug 2008 00:10:13 +0200 |
wenzelm |
of_properties: observe Markup.position_properties';
|
changeset |
files
|
| Wed, 06 Aug 2008 00:10:08 +0200 |
wenzelm |
added position_properties';
|
changeset |
files
|
| Tue, 05 Aug 2008 19:29:09 +0200 |
wenzelm |
token: maintain of source, which retains original position information;
|
changeset |
files
|
| Tue, 05 Aug 2008 19:29:08 +0200 |
wenzelm |
moved OuterLex.count here;
|
changeset |
files
|
| Tue, 05 Aug 2008 19:29:07 +0200 |
wenzelm |
improved recover: also resync on symbol/comment/verbatim delimiters;
|
changeset |
files
|
| Tue, 05 Aug 2008 19:29:06 +0200 |
wenzelm |
advance: operate on symbol list (less overhead);
|
changeset |
files
|
| Tue, 05 Aug 2008 19:29:02 +0200 |
wenzelm |
added token;
|
changeset |
files
|
| Tue, 05 Aug 2008 14:40:48 +0200 |
krauss |
fix HOL/ex/LexOrds.thy; add to regression
|
changeset |
files
|
| Tue, 05 Aug 2008 13:31:38 +0200 |
wenzelm |
added report;
|
changeset |
files
|
| Tue, 05 Aug 2008 13:31:36 +0200 |
wenzelm |
removed axiom;
|
changeset |
files
|
| Tue, 05 Aug 2008 13:31:35 +0200 |
wenzelm |
get_fact: report position;
|
changeset |
files
|
| Tue, 05 Aug 2008 13:31:31 +0200 |
wenzelm |
Facts.lookup: return static/dynamic status;
|
changeset |
files
|
| Mon, 04 Aug 2008 22:55:10 +0200 |
wenzelm |
position scanner: encode token range;
|
changeset |
files
|
| Mon, 04 Aug 2008 22:55:08 +0200 |
wenzelm |
added encode_range;
|
changeset |
files
|
| Mon, 04 Aug 2008 22:55:04 +0200 |
wenzelm |
added end_line, end_column properties;
|
changeset |
files
|
| Mon, 04 Aug 2008 22:55:00 +0200 |
wenzelm |
meta_subst: xsymbols make it work with clean Pure;
|
changeset |
files
|
| Mon, 04 Aug 2008 21:24:19 +0200 |
wenzelm |
abstract type Scan.stopper, position taken from last input token;
|
changeset |
files
|
| Mon, 04 Aug 2008 21:24:17 +0200 |
wenzelm |
abstract type Scan.stopper;
|
changeset |
files
|
| Mon, 04 Aug 2008 21:24:15 +0200 |
wenzelm |
abstract type stopper, may depend on final input;
|
changeset |
files
|
| Mon, 04 Aug 2008 20:27:40 +0200 |
wenzelm |
removed obsolete apply_theorems(_i);
|
changeset |
files
|
| Mon, 04 Aug 2008 20:27:39 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Mon, 04 Aug 2008 20:27:38 +0200 |
wenzelm |
removed obsolete note_thms_cmd;
|
changeset |
files
|
| Mon, 04 Aug 2008 20:27:37 +0200 |
wenzelm |
simplified defer_recdef(_i): plain facts via Attrib.eval_thms;
|
changeset |
files
|
| Mon, 04 Aug 2008 20:19:59 +0200 |
wenzelm |
tuned description;
|
changeset |
files
|
| Mon, 04 Aug 2008 19:25:59 +0200 |
wenzelm |
replaced mercurial.cgi by hgwebdir.cgi, resulting in http://isabelle.in.tum.de/repos/isabelle/
|
changeset |
files
|
| Mon, 04 Aug 2008 18:57:35 +0200 |
berghofe |
Quoted terms in consts_code declarations are now preprocessed as well.
|
changeset |
files
|
| Mon, 04 Aug 2008 18:56:55 +0200 |
berghofe |
Exported eval_wrapper.
|
changeset |
files
|
| Mon, 04 Aug 2008 18:56:22 +0200 |
berghofe |
- corrected bogus comment for function inst_conj_all
|
changeset |
files
|
| Mon, 04 Aug 2008 18:24:27 +0200 |
krauss |
removed dead code
|
changeset |
files
|
| Mon, 04 Aug 2008 17:13:34 +0200 |
wenzelm |
simplified prepare_command;
|
changeset |
files
|
| Mon, 04 Aug 2008 17:13:33 +0200 |
wenzelm |
Isar.command: explicitly set transaction position, as required for prepare_command errors;
|
changeset |
files
|
| Mon, 04 Aug 2008 10:37:33 +0200 |
ballarin |
Updated locale tests.
|
changeset |
files
|
| Fri, 01 Aug 2008 18:10:52 +0200 |
ballarin |
Generalised polynomial lemmas from cring to ring.
|
changeset |
files
|
| Fri, 01 Aug 2008 17:41:37 +0200 |
ballarin |
Removed import and lparams from locale record.
|
changeset |
files
|
| Fri, 01 Aug 2008 12:57:50 +0200 |
nipkow |
made setsum executable on int.
|
changeset |
files
|
| Thu, 31 Jul 2008 09:49:21 +0200 |
ballarin |
Tuned (for the sake of a meaningless log entry).
|
changeset |
files
|
| Wed, 30 Jul 2008 19:03:33 +0200 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
changeset |
files
|
| Wed, 30 Jul 2008 16:07:00 +0200 |
nipkow |
added hint about writing "x : set xs".
|
changeset |
files
|
| Wed, 30 Jul 2008 07:34:01 +0200 |
haftmann |
simple lifters
|
changeset |
files
|
| Wed, 30 Jul 2008 07:34:00 +0200 |
haftmann |
dropped imperative monad bind
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:59 +0200 |
haftmann |
facts_of
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:58 +0200 |
haftmann |
improved morphism
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:57 +0200 |
haftmann |
SML_imp, OCaml_imp
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:56 +0200 |
haftmann |
clarified
|
changeset |
files
|
| Wed, 30 Jul 2008 07:33:55 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 29 Jul 2008 17:50:48 +0200 |
ballarin |
Zorn's Lemma for partial orders.
|
changeset |
files
|
| Tue, 29 Jul 2008 17:50:12 +0200 |
ballarin |
Definitions and some lemmas for reflexive orderings.
|
changeset |
files
|
| Tue, 29 Jul 2008 17:49:26 +0200 |
ballarin |
Lemmas added
|
changeset |
files
|
| Tue, 29 Jul 2008 16:19:49 +0200 |
ballarin |
New theory on divisibility.
|
changeset |
files
|
| Tue, 29 Jul 2008 16:19:19 +0200 |
ballarin |
Renamed theorems;
|
changeset |
files
|
| Tue, 29 Jul 2008 16:17:45 +0200 |
ballarin |
New theorems on summation.
|
changeset |
files
|
| Tue, 29 Jul 2008 16:17:13 +0200 |
ballarin |
Unit_inv_l, Unit_inv_r made [simp].
|
changeset |
files
|
| Tue, 29 Jul 2008 16:16:10 +0200 |
ballarin |
New theory on divisibility;
|
changeset |
files
|
| Tue, 29 Jul 2008 16:14:56 +0200 |
ballarin |
Unit_inv_l, Unit_inv_r made [simp];
|
changeset |
files
|
| Tue, 29 Jul 2008 14:20:22 +0200 |
haftmann |
Haskell now living in the RealWorld
|
changeset |
files
|
| Tue, 29 Jul 2008 14:07:23 +0200 |
haftmann |
corrected Pure dependency
|
changeset |
files
|
| Tue, 29 Jul 2008 13:16:54 +0200 |
nipkow |
added removeAll
|
changeset |
files
|
| Tue, 29 Jul 2008 08:15:44 +0200 |
haftmann |
tuned; explicit export of element accessors
|
changeset |
files
|
| Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
changeset |
files
|
| Tue, 29 Jul 2008 08:15:39 +0200 |
haftmann |
some steps towards explicit class target for canonical interpretation
|
changeset |
files
|
| Tue, 29 Jul 2008 08:15:38 +0200 |
haftmann |
declare
|
changeset |
files
|
| Mon, 28 Jul 2008 20:49:07 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Sun, 27 Jul 2008 20:08:16 +0200 |
urbanc |
simplified a proof
|
changeset |
files
|
| Sat, 26 Jul 2008 09:00:26 +0200 |
haftmann |
tuned function name
|
changeset |
files
|
| Sat, 26 Jul 2008 09:00:25 +0200 |
haftmann |
tuned bootstrap order
|
changeset |
files
|
| Fri, 25 Jul 2008 12:03:37 +0200 |
haftmann |
subclass now also works for subclasses with empty specificaton
|
changeset |
files
|
| Fri, 25 Jul 2008 12:03:36 +0200 |
haftmann |
dropped PureThy.note; added PureThy.add_thm
|
changeset |
files
|
| Fri, 25 Jul 2008 12:03:34 +0200 |
haftmann |
added class preorder
|
changeset |
files
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
changeset |
files
|
| Fri, 25 Jul 2008 12:03:31 +0200 |
haftmann |
added explicit root theory; some tuning
|
changeset |
files
|
| Fri, 25 Jul 2008 12:03:28 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 25 Jul 2008 07:35:53 +0200 |
haftmann |
dropped locale (open)
|
changeset |
files
|
| Mon, 21 Jul 2008 16:30:49 +0200 |
haftmann |
(re-)added simp rules for (_ + _) div/mod _
|
changeset |
files
|
| Mon, 21 Jul 2008 15:27:23 +0200 |
haftmann |
(re-)added simp rules for (_ + _) div/mod _
|
changeset |
files
|
| Mon, 21 Jul 2008 15:26:26 +0200 |
haftmann |
added explicit purge_data
|
changeset |
files
|
| Mon, 21 Jul 2008 15:26:25 +0200 |
haftmann |
added code generation
|
changeset |
files
|
| Mon, 21 Jul 2008 15:26:24 +0200 |
haftmann |
fixed code generator setup
|
changeset |
files
|
| Mon, 21 Jul 2008 15:26:23 +0200 |
haftmann |
(adjusted)
|
changeset |
files
|
| Mon, 21 Jul 2008 13:37:14 +0200 |
chaieb |
Tuned and corrected ideal_tac for algebra.
|
changeset |
files
|
| Mon, 21 Jul 2008 13:37:10 +0200 |
chaieb |
Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy
|
changeset |
files
|
| Mon, 21 Jul 2008 13:37:05 +0200 |
chaieb |
Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy
|
changeset |
files
|
| Mon, 21 Jul 2008 13:36:59 +0200 |
chaieb |
Tuned and simplified proofs
|
changeset |
files
|
| Mon, 21 Jul 2008 13:36:44 +0200 |
chaieb |
Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra
|
changeset |
files
|
| Mon, 21 Jul 2008 13:36:39 +0200 |
chaieb |
Relevant rules added to algebra's context
|
changeset |
files
|
| Sun, 20 Jul 2008 23:07:03 +0200 |
wenzelm |
renamed item to span, renamed contructors;
|
changeset |
files
|
| Sun, 20 Jul 2008 23:07:01 +0200 |
wenzelm |
adapted ThyEdit.span;
|
changeset |
files
|
| Sun, 20 Jul 2008 23:06:59 +0200 |
wenzelm |
maintain token range;
|
changeset |
files
|
| Sun, 20 Jul 2008 23:06:58 +0200 |
wenzelm |
tty loop: do not report status;
|
changeset |
files
|
| Sun, 20 Jul 2008 23:06:55 +0200 |
wenzelm |
added type range;
|
changeset |
files
|
| Sun, 20 Jul 2008 23:06:53 +0200 |
wenzelm |
renamed command span markup;
|
changeset |
files
|
| Sun, 20 Jul 2008 20:23:49 +0200 |
wenzelm |
SideKickParsedData: minimal content;
|
changeset |
files
|
| Sun, 20 Jul 2008 11:19:08 +0200 |
haftmann |
(adjusted)
|
changeset |
files
|
| Sun, 20 Jul 2008 11:10:04 +0200 |
haftmann |
(adjusted)
|
changeset |
files
|
| Sat, 19 Jul 2008 19:27:13 +0200 |
bulwahn |
added verification framework for the HeapMonad and quicksort as example for this framework
|
changeset |
files
|
| Sat, 19 Jul 2008 11:05:18 +0200 |
wenzelm |
build jedit plugin only if jedit is available;
|
changeset |
files
|
| Fri, 18 Jul 2008 22:03:20 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Fri, 18 Jul 2008 18:25:57 +0200 |
haftmann |
more class instantiations
|
changeset |
files
|
| Fri, 18 Jul 2008 18:25:56 +0200 |
haftmann |
refined code generator setup for rational numbers; more simplification rules for rational numbers
|
changeset |
files
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
changeset |
files
|
| Fri, 18 Jul 2008 17:09:48 +0200 |
wenzelm |
fixed Scala path;
|
changeset |
files
|
| Thu, 17 Jul 2008 21:24:26 +0200 |
wenzelm |
tuned build order;
|
changeset |
files
|
| Thu, 17 Jul 2008 21:23:32 +0200 |
wenzelm |
proper purge_tmp;
|
changeset |
files
|
| Thu, 17 Jul 2008 21:23:08 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Thu, 17 Jul 2008 21:22:44 +0200 |
wenzelm |
tuned line breaks (NB: generated text is inserted here);
|
changeset |
files
|
| Thu, 17 Jul 2008 21:07:17 +0200 |
wenzelm |
proper usage message;
|
changeset |
files
|
| Thu, 17 Jul 2008 20:40:05 +0200 |
wenzelm |
make Isabelle source distribution (via Mercurial);
|
changeset |
files
|
| Thu, 17 Jul 2008 20:15:15 +0200 |
wenzelm |
explicit Distribution.changelog;
|
changeset |
files
|
| Thu, 17 Jul 2008 20:15:14 +0200 |
wenzelm |
structure Distribution: swapped default for is_official;
|
changeset |
files
|
| Thu, 17 Jul 2008 20:15:13 +0200 |
wenzelm |
ThyInfo.remove_thy;
|
changeset |
files
|
| Thu, 17 Jul 2008 20:15:12 +0200 |
wenzelm |
structure Distribution: swapped default for is_official;
|
changeset |
files
|
| Thu, 17 Jul 2008 20:05:19 +0200 |
wenzelm |
use ../isabelle.sty and ../isabellesym.sty;
|
changeset |
files
|
| Thu, 17 Jul 2008 17:11:34 +0200 |
wenzelm |
tuned whitespace;
|
changeset |
files
|
| Thu, 17 Jul 2008 17:10:53 +0200 |
wenzelm |
removed old checklist;
|
changeset |
files
|
| Thu, 17 Jul 2008 17:03:48 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Thu, 17 Jul 2008 17:01:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 17 Jul 2008 16:56:50 +0200 |
wenzelm |
discontinued maketags;
|
changeset |
files
|
| Thu, 17 Jul 2008 16:56:48 +0200 |
wenzelm |
assume GNU tar and find;
|
changeset |
files
|
| Thu, 17 Jul 2008 16:19:06 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 17 Jul 2008 16:17:05 +0200 |
wenzelm |
use ../isabellesym.sty, which is always available;
|
changeset |
files
|
| Thu, 17 Jul 2008 15:35:15 +0200 |
wenzelm |
Admin/build browser;
|
changeset |
files
|
| Thu, 17 Jul 2008 15:33:01 +0200 |
wenzelm |
less verbosity;
|
changeset |
files
|
| Thu, 17 Jul 2008 15:26:04 +0200 |
wenzelm |
Administrative build -- finish Isabelle source distribution.
|
changeset |
files
|
| Thu, 17 Jul 2008 15:21:52 +0200 |
krauss |
simplified proofs
|
changeset |
files
|
| Thu, 17 Jul 2008 13:50:33 +0200 |
nipkow |
beautified proofs
|
changeset |
files
|
| Thu, 17 Jul 2008 13:50:17 +0200 |
nipkow |
added lemmas
|
changeset |
files
|
| Wed, 16 Jul 2008 17:37:59 +0200 |
berghofe |
Added Standardization theory to nominal examples.
|
changeset |
files
|
| Wed, 16 Jul 2008 17:36:44 +0200 |
berghofe |
Added Standardization theory.
|
changeset |
files
|
| Wed, 16 Jul 2008 16:42:13 +0200 |
wenzelm |
editor model: run interactively for now;
|
changeset |
files
|
| Wed, 16 Jul 2008 16:39:11 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Wed, 16 Jul 2008 16:17:26 +0200 |
wenzelm |
identify: more informative id in Toplevel.debug mode;
|
changeset |
files
|
| Wed, 16 Jul 2008 14:28:47 +0200 |
wenzelm |
shortlogentry/filelogentry: show shortdate and full description;
|
changeset |
files
|
| Wed, 16 Jul 2008 14:21:57 +0200 |
ballarin |
Removed uses of context element includes.
|
changeset |
files
|
| Wed, 16 Jul 2008 11:20:25 +0200 |
wenzelm |
added Isar.command, Isar.insert, Isar.remove (editor model);
|
changeset |
files
|
| Wed, 16 Jul 2008 11:20:24 +0200 |
wenzelm |
export type id with no_id and create_command;
|
changeset |
files
|
| Tue, 15 Jul 2008 23:36:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 15 Jul 2008 22:37:58 +0200 |
wenzelm |
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
|
changeset |
files
|
| Tue, 15 Jul 2008 22:37:55 +0200 |
wenzelm |
load thy_edit.ML before isar.ML;
|
changeset |
files
|
| Tue, 15 Jul 2008 19:39:37 +0200 |
wenzelm |
modernized specifications and proofs;
|
changeset |
files
|
| Tue, 15 Jul 2008 16:50:09 +0200 |
ballarin |
Removed uses of context element includes.
|
changeset |
files
|
| Tue, 15 Jul 2008 16:02:10 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 15 Jul 2008 16:02:07 +0200 |
haftmann |
tuned code theorem bookkeeping
|
changeset |
files
|
| Tue, 15 Jul 2008 15:59:49 +0200 |
wenzelm |
tuned changelogentry;
|
changeset |
files
|
| Tue, 15 Jul 2008 15:46:43 +0200 |
wenzelm |
refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);
|
changeset |
files
|
| Tue, 15 Jul 2008 15:46:41 +0200 |
wenzelm |
support for command status;
|
changeset |
files
|
| Tue, 15 Jul 2008 14:15:49 +0200 |
wenzelm |
added status channel;
|
changeset |
files
|
| Tue, 15 Jul 2008 14:15:43 +0200 |
wenzelm |
added status channel;
|
changeset |
files
|
| Tue, 15 Jul 2008 12:13:14 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 15 Jul 2008 11:50:04 +0200 |
wenzelm |
simplified commit_exit;
|
changeset |
files
|
| Tue, 15 Jul 2008 11:50:03 +0200 |
wenzelm |
simplified commit_exit: operate on previous node of final state, include warning here;
|
changeset |
files
|
| Tue, 15 Jul 2008 11:50:02 +0200 |
wenzelm |
removed obsolete commit_exit;
|
changeset |
files
|
| Tue, 15 Jul 2008 11:02:43 +0200 |
wenzelm |
added command 'linear_undo';
|
changeset |
files
|
| Tue, 15 Jul 2008 10:59:14 +0200 |
wenzelm |
removed command 'redo';
|
changeset |
files
|
| Tue, 15 Jul 2008 10:49:39 +0200 |
wenzelm |
adapted ThyInfo.end_theory;
|
changeset |
files
|
| Tue, 15 Jul 2008 09:30:39 +0200 |
haftmann |
dropped map; fixed swap
|
changeset |
files
|
| Tue, 15 Jul 2008 07:10:50 +0200 |
haftmann |
curried gcd
|
changeset |
files
|
| Mon, 14 Jul 2008 23:28:26 +0200 |
wenzelm |
cover macbroy as well;
|
changeset |
files
|
| Mon, 14 Jul 2008 23:11:20 +0200 |
wenzelm |
tuned filelogentry;
|
changeset |
files
|
| Mon, 14 Jul 2008 22:55:48 +0200 |
wenzelm |
print_mode "test_markup": do not change prompt, otherwise Proof General will not work;
|
changeset |
files
|
| Mon, 14 Jul 2008 22:26:53 +0200 |
wenzelm |
tuned message;
|
changeset |
files
|
| Mon, 14 Jul 2008 22:09:08 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Mon, 14 Jul 2008 21:39:08 +0200 |
wenzelm |
inform_file_processed: Isar.init_point last!
|
changeset |
files
|
| Mon, 14 Jul 2008 21:07:57 +0200 |
wenzelm |
removed HOL-Complex, which has been discontinued after Isabelle2008;
|
changeset |
files
|
| Mon, 14 Jul 2008 19:59:58 +0200 |
wenzelm |
added HOL-Nominal image;
|
changeset |
files
|
| Mon, 14 Jul 2008 19:57:14 +0200 |
wenzelm |
removed obsolete Pure/General/history.ML;
|
changeset |
files
|
| Mon, 14 Jul 2008 19:57:13 +0200 |
wenzelm |
inform_file_processed: try harder not to fail, ensure
|
changeset |
files
|
| Mon, 14 Jul 2008 19:57:11 +0200 |
wenzelm |
commit_exit: proper error;
|
changeset |
files
|
| Mon, 14 Jul 2008 19:57:09 +0200 |
wenzelm |
export EXCURSION_FAIL;
|
changeset |
files
|
| Mon, 14 Jul 2008 19:20:57 +0200 |
haftmann |
dropped junk
|
changeset |
files
|
| Mon, 14 Jul 2008 19:20:29 +0200 |
haftmann |
moved bootstrap of simplifier
|
changeset |
files
|
| Mon, 14 Jul 2008 19:20:28 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:48 +0200 |
wenzelm |
end_theory: no result;
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:47 +0200 |
wenzelm |
removed obsolete Toplevel.RESTART;
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:44 +0200 |
wenzelm |
proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML);
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:43 +0200 |
wenzelm |
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:42 +0200 |
wenzelm |
adapted IsarCmd.init_theory;
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:41 +0200 |
wenzelm |
renamed theory to init_theory, removed obsolete kill argument;
|
changeset |
files
|
| Mon, 14 Jul 2008 17:51:39 +0200 |
wenzelm |
added commit_exit;
|
changeset |
files
|
| Mon, 14 Jul 2008 17:47:18 +0200 |
krauss |
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
|
changeset |
files
|
| Mon, 14 Jul 2008 17:02:55 +0200 |
krauss |
renamed conversions to _conv, tuned
|
changeset |
files
|
| Mon, 14 Jul 2008 16:13:58 +0200 |
chaieb |
Simplified proofs
|
changeset |
files
|
| Mon, 14 Jul 2008 16:13:55 +0200 |
chaieb |
Simple theorems about zgcd moved to GCD.thy
|
changeset |
files
|
| Mon, 14 Jul 2008 16:13:51 +0200 |
chaieb |
Theorem names as in IntPrimes.thy, also several theorems moved from there
|
changeset |
files
|
| Mon, 14 Jul 2008 16:13:42 +0200 |
chaieb |
Fixed proofs.
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:43 +0200 |
wenzelm |
ProofNode.current
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:42 +0200 |
wenzelm |
command 'redo' no longer available;
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:41 +0200 |
wenzelm |
replaced obsolete ProofHistory by ProofNode (backtracking only);
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:40 +0200 |
wenzelm |
removed obsolete 'redo' command;
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:39 +0200 |
wenzelm |
removed obsolete history commands;
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:38 +0200 |
wenzelm |
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:37 +0200 |
wenzelm |
obsolete (cf. proof_node.ML);
|
changeset |
files
|
| Mon, 14 Jul 2008 11:19:36 +0200 |
wenzelm |
removed Isar/proof_history.ML;
|
changeset |
files
|
| Mon, 14 Jul 2008 11:04:47 +0200 |
haftmann |
added further simple interfaces
|
changeset |
files
|
| Mon, 14 Jul 2008 11:04:46 +0200 |
haftmann |
simpsets as pre/postprocessors; generic preprocessor now named function transformators
|
changeset |
files
|
| Mon, 14 Jul 2008 11:04:42 +0200 |
haftmann |
unified curried gcd, lcm, zgcd, zlcm
|
changeset |
files
|
| Fri, 11 Jul 2008 23:17:25 +0200 |
wenzelm |
Sorts.weaken: abstract argument;
|
changeset |
files
|
| Fri, 11 Jul 2008 23:17:23 +0200 |
wenzelm |
Sorts.weaken: abstract argument;
|
changeset |
files
|
| Fri, 11 Jul 2008 16:56:20 +0200 |
huffman |
instance real_field < field_char_0;
|
changeset |
files
|
| Fri, 11 Jul 2008 09:03:25 +0200 |
haftmann |
re-removed subclass relation real_field < field_char_0: coregularity violation in NSA/HyperDef
|
changeset |
files
|
| Fri, 11 Jul 2008 09:03:11 +0200 |
haftmann |
Fract now total; improved code generator setup
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:33 +0200 |
haftmann |
simple inheritance concept
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:32 +0200 |
haftmann |
tuned thyname lookup
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:31 +0200 |
haftmann |
fixed layout
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:30 +0200 |
haftmann |
explicit completions of arities
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:29 +0200 |
haftmann |
tuned order
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:28 +0200 |
haftmann |
antiquotation
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:27 +0200 |
haftmann |
improved code generator setup
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:26 +0200 |
haftmann |
explicit dependency
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:24 +0200 |
haftmann |
class instead of axclass
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:23 +0200 |
haftmann |
tuned import
|
changeset |
files
|
| Fri, 11 Jul 2008 09:02:22 +0200 |
haftmann |
separate class dvd for divisibility predicate
|
changeset |
files
|
| Fri, 11 Jul 2008 00:35:19 +0200 |
kleing |
temporarily disable at-sml-dev-p
|
changeset |
files
|
| Thu, 10 Jul 2008 22:47:26 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Thu, 10 Jul 2008 21:12:34 +0200 |
wenzelm |
restart: Isar.init_point;
|
changeset |
files
|
| Thu, 10 Jul 2008 21:03:47 +0200 |
wenzelm |
proper_inform_file_processed: Isar.init_point starts fresh command sequence;
|
changeset |
files
|
| Thu, 10 Jul 2008 20:54:00 +0200 |
wenzelm |
activated new versions of undo, kill_proof;
|
changeset |
files
|
| Thu, 10 Jul 2008 20:53:52 +0200 |
wenzelm |
activated new versions of init_toplevel, linear_undo, undo, undos_proof kill;
|
changeset |
files
|
| Thu, 10 Jul 2008 20:53:50 +0200 |
wenzelm |
added print;
|
changeset |
files
|
| Thu, 10 Jul 2008 20:03:30 +0200 |
wenzelm |
added ProofGeneral.isar_kill_proof;
|
changeset |
files
|
| Thu, 10 Jul 2008 20:03:28 +0200 |
wenzelm |
added Isar.init_point, Isar.kill;
|
changeset |
files
|
| Thu, 10 Jul 2008 20:02:55 +0200 |
wenzelm |
export init_point;
|
changeset |
files
|
| Thu, 10 Jul 2008 18:02:34 +0200 |
wenzelm |
added Isar.linear_undo;
|
changeset |
files
|
| Thu, 10 Jul 2008 17:47:40 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 10 Jul 2008 17:43:02 +0200 |
wenzelm |
tty interaction: do not move point after error;
|
changeset |
files
|
| Thu, 10 Jul 2008 17:26:27 +0200 |
wenzelm |
change_lexicons: no verbosity;
|
changeset |
files
|
| Thu, 10 Jul 2008 17:26:25 +0200 |
wenzelm |
added Isar.undo, which emulates old-style undo on global tty state;
|
changeset |
files
|
| Thu, 10 Jul 2008 17:26:23 +0200 |
wenzelm |
provide old-style undo operation (still unused);
|
changeset |
files
|
| Thu, 10 Jul 2008 17:26:22 +0200 |
wenzelm |
added prompt markup;
|
changeset |
files
|
| Thu, 10 Jul 2008 13:37:35 +0200 |
wenzelm |
@{lemma}: allow terminal method;
|
changeset |
files
|
| Thu, 10 Jul 2008 13:37:34 +0200 |
wenzelm |
@{lemma}: allow terminal method, close derivation unless (open) mode is given;
|
changeset |
files
|
| Thu, 10 Jul 2008 13:37:33 +0200 |
wenzelm |
added is_diag;
|
changeset |
files
|
| Thu, 10 Jul 2008 13:37:31 +0200 |
wenzelm |
slightly improved @{lemma} (both for latex and ML);
|
changeset |
files
|
| Thu, 10 Jul 2008 11:17:16 +0200 |
wenzelm |
misc tuning;
|
changeset |
files
|
| Thu, 10 Jul 2008 10:58:36 +0200 |
ballarin |
Fixed (harmless) typo in closing *}.
|
changeset |
files
|
| Thu, 10 Jul 2008 07:15:19 +0200 |
huffman |
by intro_locales -> ..
|
changeset |
files
|
| Thu, 10 Jul 2008 07:07:54 +0200 |
huffman |
instance real_field < field_char_0
|
changeset |
files
|
| Wed, 09 Jul 2008 22:33:35 +0200 |
huffman |
remove redundant lemmas about cmod
|
changeset |
files
|
| Wed, 09 Jul 2008 22:32:17 +0200 |
wenzelm |
removed owner;
|
changeset |
files
|
| Wed, 09 Jul 2008 22:25:24 +0200 |
wenzelm |
tuned description;
|
changeset |
files
|
| Wed, 09 Jul 2008 22:23:34 +0200 |
wenzelm |
changes wrt. gitweb style;
|
changeset |
files
|
| Wed, 09 Jul 2008 22:13:09 +0200 |
wenzelm |
style = isabelle (based on gitweb);
|
changeset |
files
|
| Wed, 09 Jul 2008 20:18:06 +0200 |
huffman |
rearrange instantiations
|
changeset |
files
|
| Wed, 09 Jul 2008 17:14:31 +0200 |
wenzelm |
added get_first;
|
changeset |
files
|
| Tue, 08 Jul 2008 23:20:07 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 08 Jul 2008 23:14:35 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 08 Jul 2008 22:25:12 +0200 |
huffman |
fix more typos
|
changeset |
files
|
| Tue, 08 Jul 2008 22:07:39 +0200 |
huffman |
fix another typo
|
changeset |
files
|
| Tue, 08 Jul 2008 22:02:15 +0200 |
huffman |
fix typo
|
changeset |
files
|
| Tue, 08 Jul 2008 21:55:41 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Tue, 08 Jul 2008 21:15:23 +0200 |
wenzelm |
global commands: explicit graph;
|
changeset |
files
|
| Tue, 08 Jul 2008 20:42:00 +0200 |
wenzelm |
export str_of;
|
changeset |
files
|
| Tue, 08 Jul 2008 18:13:12 +0200 |
haftmann |
clarified code
|
changeset |
files
|
| Tue, 08 Jul 2008 18:13:11 +0200 |
haftmann |
exported weaken combinator
|
changeset |
files
|
| Tue, 08 Jul 2008 18:13:10 +0200 |
haftmann |
refined arity property concept
|
changeset |
files
|
| Tue, 08 Jul 2008 18:13:09 +0200 |
haftmann |
fix: using IntInf.int for SML
|
changeset |
files
|
| Tue, 08 Jul 2008 17:52:28 +0200 |
wenzelm |
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
|
changeset |
files
|
| Tue, 08 Jul 2008 17:52:26 +0200 |
wenzelm |
removed obsolete touch_child_thys;
|
changeset |
files
|
| Tue, 08 Jul 2008 17:52:24 +0200 |
wenzelm |
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
|
changeset |
files
|
| Tue, 08 Jul 2008 17:48:17 +0200 |
wenzelm |
more qualified ThyInfo names;
|
changeset |
files
|
| Tue, 08 Jul 2008 16:19:24 +0200 |
wenzelm |
begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
|
changeset |
files
|
| Tue, 08 Jul 2008 16:19:23 +0200 |
wenzelm |
removed unused href_opt_name;
|
changeset |
files
|
| Tue, 08 Jul 2008 13:45:27 +0200 |
kleing |
migrated at-sml-dev-p to macbroy24, hoping for more reliable hardware
|
changeset |
files
|
| Mon, 07 Jul 2008 23:37:33 +0200 |
kleing |
retired mac-sml-dev.
|
changeset |
files
|
| Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
changeset |
files
|
| Fri, 04 Jul 2008 16:33:08 +0200 |
huffman |
prefer theorem names without numbers
|
changeset |
files
|
| Fri, 04 Jul 2008 15:57:55 +0200 |
huffman |
HOL-NSA
|
changeset |
files
|
| Fri, 04 Jul 2008 07:39:01 +0200 |
haftmann |
added marginal setup for code generation
|
changeset |
files
|
| Thu, 03 Jul 2008 20:53:44 +0200 |
huffman |
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
|
changeset |
files
|
| Thu, 03 Jul 2008 20:15:06 +0200 |
wenzelm |
removed old NSPrimes, cf. NSA/Examples/;
|
changeset |
files
|
| Thu, 03 Jul 2008 20:10:52 +0200 |
wenzelm |
cvsps: back to non-verbose mode;
|
changeset |
files
|
| Thu, 03 Jul 2008 19:50:19 +0200 |
wenzelm |
removed old Complex/ex/NSPrimes.thy;
|
changeset |
files
|
| Thu, 03 Jul 2008 19:47:05 +0200 |
wenzelm |
maxfiles = 50;
|
changeset |
files
|
| Thu, 03 Jul 2008 19:17:52 +0200 |
wenzelm |
more sessions;
|
changeset |
files
|
| Thu, 03 Jul 2008 19:17:29 +0200 |
wenzelm |
more precise dependencies for HOL-Word and HOL-NSA;
|
changeset |
files
|
| Thu, 03 Jul 2008 19:02:33 +0200 |
huffman |
fixed extremely slow proof of Chain_inits_DiffI
|
changeset |
files
|
| Thu, 03 Jul 2008 18:16:40 +0200 |
huffman |
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
|
changeset |
files
|
| Thu, 03 Jul 2008 18:15:39 +0200 |
huffman |
move proofs of add_left_cancel and add_right_cancel into the correct locale
|
changeset |
files
|
| Thu, 03 Jul 2008 18:03:10 +0200 |
wenzelm |
cvsps -v (verbose);
|
changeset |
files
|
| Thu, 03 Jul 2008 17:58:10 +0200 |
huffman |
removed nonstandard analysis theories to HOL-NSA
|
changeset |
files
|
| Thu, 03 Jul 2008 17:57:01 +0200 |
huffman |
moved theories to HOL/NSA
|
changeset |
files
|
| Thu, 03 Jul 2008 17:53:39 +0200 |
huffman |
add HOL-NSA
|
changeset |
files
|
| Thu, 03 Jul 2008 17:51:53 +0200 |
wenzelm |
use patched cvsps to workaround loss of "foo: bar;" log entries;
|
changeset |
files
|
| Thu, 03 Jul 2008 17:47:22 +0200 |
huffman |
move nonstandard analysis theories to NSA directory
|
changeset |
files
|
| Thu, 03 Jul 2008 15:37:10 +0200 |
wenzelm |
back to default style, which shows files in changelog view;
|
changeset |
files
|
| Thu, 03 Jul 2008 15:13:59 +0200 |
wenzelm |
added description;
|
changeset |
files
|
| Thu, 03 Jul 2008 14:52:54 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 03 Jul 2008 14:44:49 +0200 |
wenzelm |
logrotate setup;
|
changeset |
files
|
| Thu, 03 Jul 2008 14:34:53 +0200 |
wenzelm |
redirect stderr as well;
|
changeset |
files
|
| Thu, 03 Jul 2008 14:31:19 +0200 |
wenzelm |
output to log file;
|
changeset |
files
|
| Thu, 03 Jul 2008 13:17:19 +0200 |
wenzelm |
specific to CVS;
|
changeset |
files
|
| Thu, 03 Jul 2008 13:04:30 +0200 |
wenzelm |
Isabelle repository service.
|
changeset |
files
|
| Thu, 03 Jul 2008 12:56:43 +0200 |
wenzelm |
ensure hg/.hg/hgrc;
|
changeset |
files
|
| Thu, 03 Jul 2008 12:54:12 +0200 |
wenzelm |
hgrc for conversion and web service;
|
changeset |
files
|
| Thu, 03 Jul 2008 12:53:38 +0200 |
wenzelm |
provide HGRCPATH, taken from cvs/Admin;
|
changeset |
files
|
| Thu, 03 Jul 2008 11:16:33 +0200 |
haftmann |
code antiquotation roaring ahead
|
changeset |
files
|
| Thu, 03 Jul 2008 11:16:09 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 03 Jul 2008 11:16:08 +0200 |
haftmann |
adjusted postprocessort setup
|
changeset |
files
|
| Thu, 03 Jul 2008 11:16:07 +0200 |
haftmann |
added lemma antiquotation
|
changeset |
files
|
| Thu, 03 Jul 2008 11:16:05 +0200 |
haftmann |
adjusted rep_datatype
|
changeset |
files
|
| Thu, 03 Jul 2008 00:58:30 +0200 |
berghofe |
Adapted to changes in perm_simp / swap_simps.
|
changeset |
files
|
| Thu, 03 Jul 2008 00:56:45 +0200 |
berghofe |
Replaced all but one occurrence of perm_simp_tac by perm_simproc_app,
|
changeset |
files
|
| Thu, 03 Jul 2008 00:54:45 +0200 |
berghofe |
Rewrote code to use swap_simps rather than calc_atm (which tends to
|
changeset |
files
|
| Wed, 02 Jul 2008 21:43:57 +0200 |
wenzelm |
moved HOL-Plain up;
|
changeset |
files
|
| Wed, 02 Jul 2008 20:31:06 +0200 |
wenzelm |
rename Doc doc-src;
|
changeset |
files
|
| Wed, 02 Jul 2008 20:13:32 +0200 |
wenzelm |
renamed Contents to Dirs to avoid case-conflict with doc/Contents;
|
changeset |
files
|
| Wed, 02 Jul 2008 19:52:57 +0200 |
huffman |
section -> subsection
|
changeset |
files
|
| Wed, 02 Jul 2008 19:52:38 +0200 |
wenzelm |
convert Isabelle CVS to Mercurial;
|
changeset |
files
|
| Wed, 02 Jul 2008 19:35:43 +0200 |
huffman |
use begin and end for proofs in locales
|
changeset |
files
|
| Wed, 02 Jul 2008 18:13:10 +0200 |
wenzelm |
exclude Distribution/bin/Isabelle;
|
changeset |
files
|
| Wed, 02 Jul 2008 16:40:20 +0200 |
wenzelm |
init_theory: pass name explicitly;
|
changeset |
files
|
| Wed, 02 Jul 2008 16:40:18 +0200 |
wenzelm |
replaced datatype category constructivism by is_theory/is_proof;
|
changeset |
files
|
| Wed, 02 Jul 2008 16:40:17 +0200 |
wenzelm |
Toplevel.init_theory: pass name explicitly;
|
changeset |
files
|
| Wed, 02 Jul 2008 16:40:15 +0200 |
wenzelm |
command: always keep transition, not just as initial status;
|
changeset |
files
|
| Wed, 02 Jul 2008 11:47:27 +0200 |
haftmann |
cached code for code antiquotation
|
changeset |
files
|
| Wed, 02 Jul 2008 07:12:17 +0200 |
haftmann |
code antiquotation roaring ahead
|
changeset |
files
|
| Wed, 02 Jul 2008 07:11:57 +0200 |
haftmann |
cleaned up some code generator configuration
|
changeset |
files
|
| Tue, 01 Jul 2008 21:30:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 01 Jul 2008 21:30:11 +0200 |
wenzelm |
added datatype category;
|
changeset |
files
|
| Tue, 01 Jul 2008 21:30:08 +0200 |
wenzelm |
replaced datatype kind by OuterKeyword.category;
|
changeset |
files
|
| Tue, 01 Jul 2008 21:20:18 +0200 |
wenzelm |
clean: HOL-Plain;
|
changeset |
files
|
| Tue, 01 Jul 2008 20:26:48 +0200 |
huffman |
prove lemma finite in context of finite class
|
changeset |
files
|
| Tue, 01 Jul 2008 20:10:59 +0200 |
wenzelm |
added HOL-Plain;
|
changeset |
files
|
| Tue, 01 Jul 2008 18:38:44 +0200 |
wenzelm |
explicit identification of toplevel commands, with status etc.;
|
changeset |
files
|
| Tue, 01 Jul 2008 18:38:43 +0200 |
wenzelm |
added name_of;
|
changeset |
files
|
| Tue, 01 Jul 2008 18:38:41 +0200 |
wenzelm |
added get_id/put_id;
|
changeset |
files
|
| Tue, 01 Jul 2008 09:58:32 +0200 |
haftmann |
(removed Complex/ROOT.ML)
|
changeset |
files
|
| Tue, 01 Jul 2008 08:19:00 +0200 |
haftmann |
HOL += HOL-Complex
|
changeset |
files
|
| Tue, 01 Jul 2008 08:05:08 +0200 |
haftmann |
HOL += HOL-Complex
|
changeset |
files
|
| Tue, 01 Jul 2008 07:58:37 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Tue, 01 Jul 2008 07:58:17 +0200 |
haftmann |
HOL += HOL-Complex
|
changeset |
files
|
| Tue, 01 Jul 2008 07:13:45 +0200 |
huffman |
put file dependencies on separate lines
|
changeset |
files
|
| Tue, 01 Jul 2008 06:56:37 +0200 |
huffman |
range_composition no longer in simp set
|
changeset |
files
|
| Tue, 01 Jul 2008 06:51:59 +0200 |
huffman |
remove simp attribute from range_composition
|
changeset |
files
|
| Tue, 01 Jul 2008 06:21:28 +0200 |
huffman |
rename INF to INFM
|
changeset |
files
|
| Tue, 01 Jul 2008 03:14:00 +0200 |
huffman |
remove unused lemmas ub2ub_monofun' and dir2dir_monofun
|
changeset |
files
|
| Tue, 01 Jul 2008 03:12:39 +0200 |
huffman |
remove redundant instance proof finite_po < cpo
|
changeset |
files
|
| Tue, 01 Jul 2008 02:50:29 +0200 |
huffman |
remove unused lemma is_lub_Iup'
|
changeset |
files
|
| Tue, 01 Jul 2008 02:19:53 +0200 |
huffman |
replace lub (range Y) with (LUB i. Y i)
|
changeset |
files
|
| Tue, 01 Jul 2008 01:28:44 +0200 |
huffman |
add file dependencies
|
changeset |
files
|
| Tue, 01 Jul 2008 01:28:07 +0200 |
huffman |
universal bifinite domain
|
changeset |
files
|
| Tue, 01 Jul 2008 01:26:20 +0200 |
huffman |
isomorphisms between naturals and sums, products, and finite sets
|
changeset |
files
|
| Tue, 01 Jul 2008 01:25:40 +0200 |
huffman |
theory of algebraic deflations
|
changeset |
files
|
| Tue, 01 Jul 2008 01:25:16 +0200 |
huffman |
theory of eventually-constant sequences
|
changeset |
files
|
| Tue, 01 Jul 2008 01:19:08 +0200 |
huffman |
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
|
changeset |
files
|
| Tue, 01 Jul 2008 01:09:03 +0200 |
huffman |
rename compact_approx to compact_take
|
changeset |
files
|
| Tue, 01 Jul 2008 00:58:19 +0200 |
huffman |
rename approx_pd to pd_take
|
changeset |
files
|
| Tue, 01 Jul 2008 00:52:46 +0200 |
huffman |
split Completion.thy from CompactBasis.thy
|
changeset |
files
|
| Mon, 30 Jun 2008 22:24:27 +0200 |
wenzelm |
filemap for CVS -> Mercurial conversion;
|
changeset |
files
|
| Mon, 30 Jun 2008 22:16:47 +0200 |
huffman |
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
|
changeset |
files
|
| Mon, 30 Jun 2008 21:52:17 +0200 |
huffman |
New theory of deflations and embedding-projection pairs
|
changeset |
files
|
| Mon, 30 Jun 2008 21:47:56 +0200 |
huffman |
remove unused Cset.thy
|
changeset |
files
|
| Mon, 30 Jun 2008 14:06:44 +0200 |
urbanc |
added facts to lemma swap_simps and tuned lemma calc_atms
|
changeset |
files
|
| Mon, 30 Jun 2008 13:41:33 +0200 |
haftmann |
simplified retrieval of theory names of consts and types
|
changeset |
files
|
| Mon, 30 Jun 2008 13:41:31 +0200 |
haftmann |
tagged arities
|
changeset |
files
|
| Mon, 30 Jun 2008 13:41:30 +0200 |
haftmann |
HOL-Complex with proof terms
|
changeset |
files
|
| Mon, 30 Jun 2008 13:41:28 +0200 |
haftmann |
code generator setup for "int" also works under eta-contraction
|
changeset |
files
|
| Sat, 28 Jun 2008 23:52:43 +0200 |
wenzelm |
added ML/ml_thms.ML;
|
changeset |
files
|
| Sat, 28 Jun 2008 22:58:49 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Jun 2008 22:56:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Jun 2008 22:54:19 +0200 |
wenzelm |
additional ML antiquotations;
|
changeset |
files
|
| Sat, 28 Jun 2008 22:52:11 +0200 |
wenzelm |
moved theorem values to ml_thms.ML;
|
changeset |
files
|
| Sat, 28 Jun 2008 22:52:07 +0200 |
wenzelm |
Isar theorem values within ML.
|
changeset |
files
|
| Sat, 28 Jun 2008 22:52:03 +0200 |
wenzelm |
added ML/ml_thms.ML;
|
changeset |
files
|
| Sat, 28 Jun 2008 22:52:01 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Sat, 28 Jun 2008 21:21:21 +0200 |
wenzelm |
allow overlap of minor keywords and commands;
|
changeset |
files
|
| Sat, 28 Jun 2008 21:21:20 +0200 |
wenzelm |
include HOL-Plain;
|
changeset |
files
|
| Sat, 28 Jun 2008 21:21:18 +0200 |
wenzelm |
tuned args parser (cf. args.ML);
|
changeset |
files
|
| Sat, 28 Jun 2008 21:21:17 +0200 |
wenzelm |
replaced simple_text by fully-featured parse_args;
|
changeset |
files
|
| Sat, 28 Jun 2008 21:21:15 +0200 |
wenzelm |
tuned nested args parser;
|
changeset |
files
|
| Sat, 28 Jun 2008 21:21:13 +0200 |
wenzelm |
@{lemma}: 'by' keyword;
|
changeset |
files
|
| Sat, 28 Jun 2008 15:30:46 +0200 |
wenzelm |
ML: improved antiquotations;
|
changeset |
files
|
| Sat, 28 Jun 2008 15:17:28 +0200 |
wenzelm |
added macro interface;
|
changeset |
files
|
| Sat, 28 Jun 2008 15:17:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 28 Jun 2008 15:17:24 +0200 |
wenzelm |
added thm_name, opt_thm_name;
|
changeset |
files
|
| Fri, 27 Jun 2008 09:55:02 +0200 |
haftmann |
adjusted import
|
changeset |
files
|
| Fri, 27 Jun 2008 09:34:08 +0200 |
haftmann |
adjusted import
|
changeset |
files
|
| Fri, 27 Jun 2008 00:37:30 +0200 |
urbanc |
added a lemma to at_swap_simps
|
changeset |
files
|
| Thu, 26 Jun 2008 17:54:05 +0200 |
huffman |
remove cset theory; define ideal completions using typedef instead of cpodef
|
changeset |
files
|
| Thu, 26 Jun 2008 15:06:30 +0200 |
wenzelm |
Args.theory;
|
changeset |
files
|
| Thu, 26 Jun 2008 15:06:28 +0200 |
wenzelm |
added context/theory scanner;
|
changeset |
files
|
| Thu, 26 Jun 2008 15:06:25 +0200 |
wenzelm |
Args.context;
|
changeset |
files
|
| Thu, 26 Jun 2008 11:58:27 +0200 |
krauss |
fix: need to beta/eta normalize
|
changeset |
files
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
changeset |
files
|
| Thu, 26 Jun 2008 10:06:54 +0200 |
haftmann |
added dummy citiation
|
changeset |
files
|
| Thu, 26 Jun 2008 10:06:53 +0200 |
haftmann |
dropped recdef
|
changeset |
files
|
| Thu, 26 Jun 2008 10:06:51 +0200 |
haftmann |
class theory name lookup improved
|
changeset |
files
|
| Wed, 25 Jun 2008 22:11:17 +0200 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Wed, 25 Jun 2008 22:01:35 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Wed, 25 Jun 2008 22:01:34 +0200 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Wed, 25 Jun 2008 21:25:51 +0200 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Wed, 25 Jun 2008 18:23:50 +0200 |
urbanc |
typo
|
changeset |
files
|
| Wed, 25 Jun 2008 17:38:39 +0200 |
wenzelm |
re-use official outer keywords;
|
changeset |
files
|
| Wed, 25 Jun 2008 17:38:38 +0200 |
wenzelm |
scan: prefer command over keyword, allowing lexicons to overlap;
|
changeset |
files
|
| Wed, 25 Jun 2008 17:38:37 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
changeset |
files
|
| Wed, 25 Jun 2008 17:38:36 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
changeset |
files
|
| Wed, 25 Jun 2008 17:38:35 +0200 |
wenzelm |
antiquote: need to quote outer keywords;
|
changeset |
files
|
| Wed, 25 Jun 2008 17:38:34 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 25 Jun 2008 17:38:32 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
changeset |
files
|
| Wed, 25 Jun 2008 14:54:45 +0200 |
berghofe |
- Equivariance simpset used in proofs of strong induction and inversion
|
changeset |
files
|
| Wed, 25 Jun 2008 12:15:05 +0200 |
wenzelm |
pprint: back to proper output of markup, with workaround for Poly/ML crash;
|
changeset |
files
|
| Tue, 24 Jun 2008 23:38:44 +0200 |
wenzelm |
back to 1.36 (Poly/ML crash!?);
|
changeset |
files
|
| Tue, 24 Jun 2008 22:27:36 +0200 |
wenzelm |
updated generated file;
|
changeset |
files
|