| Sat, 03 Sep 2005 18:00:48 +0200 |
wenzelm |
tuned msg;
|
changeset |
files
|
| Sat, 03 Sep 2005 17:56:48 +0200 |
wenzelm |
uses ("LCF_lemmas.ML");
|
changeset |
files
|
| Sat, 03 Sep 2005 17:54:10 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sat, 03 Sep 2005 17:54:07 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 03 Sep 2005 17:54:05 +0200 |
wenzelm |
removed fix.thy, pair.thy, simpdata.ML;
|
changeset |
files
|
| Sat, 03 Sep 2005 17:15:51 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sat, 03 Sep 2005 16:50:22 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sat, 03 Sep 2005 16:49:48 +0200 |
wenzelm |
setmp print_mode []; more robust outer syntax; tuned;
|
changeset |
files
|
| Sat, 03 Sep 2005 16:48:45 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 03 Sep 2005 16:47:25 +0200 |
wenzelm |
simplified oracle;
|
changeset |
files
|
| Sat, 03 Sep 2005 16:46:56 +0200 |
wenzelm |
use Check.ML;
|
changeset |
files
|
| Sat, 03 Sep 2005 16:46:20 +0200 |
wenzelm |
fixed ML errors;
|
changeset |
files
|
| Sat, 03 Sep 2005 16:45:43 +0200 |
wenzelm |
removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML;
|
changeset |
files
|
| Sat, 03 Sep 2005 16:44:17 +0200 |
wenzelm |
deprecated non-Isar theory file format;
|
changeset |
files
|
| Fri, 02 Sep 2005 21:29:55 +0200 |
quigley |
Added ECommunication.ML
|
changeset |
files
|
| Fri, 02 Sep 2005 21:29:33 +0200 |
quigley |
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
|
changeset |
files
|
| Fri, 02 Sep 2005 17:55:24 +0200 |
paulson |
further tidying up of Isabelle-ATP link
|
changeset |
files
|
| Fri, 02 Sep 2005 17:23:59 +0200 |
wenzelm |
converted specifications to Isar theories;
|
changeset |
files
|
| Fri, 02 Sep 2005 15:54:47 +0200 |
haftmann |
some 'assoc' etc. refactoring
|
changeset |
files
|
| Fri, 02 Sep 2005 15:25:44 +0200 |
paulson |
tidying up the Isabelle/ATP interface
|
changeset |
files
|
| Fri, 02 Sep 2005 15:25:27 +0200 |
paulson |
fixed arities and restored changes that had gone missing
|
changeset |
files
|
| Fri, 02 Sep 2005 15:24:58 +0200 |
paulson |
deleted obsolete VampireCommunication.ML
|
changeset |
files
|
| Fri, 02 Sep 2005 09:50:58 +0200 |
ballarin |
print_locale omits facts by default
|
changeset |
files
|
| Thu, 01 Sep 2005 23:08:15 +0200 |
wenzelm |
curried_lookup/update;
|
changeset |
files
|
| Thu, 01 Sep 2005 22:49:18 +0200 |
wenzelm |
refrain from sorting output;
|
changeset |
files
|
| Thu, 01 Sep 2005 22:15:14 +0200 |
wenzelm |
curried_lookup/update;
|
changeset |
files
|
| Thu, 01 Sep 2005 22:15:12 +0200 |
wenzelm |
curried_lookup/update;
|
changeset |
files
|
| Thu, 01 Sep 2005 22:15:10 +0200 |
wenzelm |
curried_lookup/update;
|
changeset |
files
|
| Thu, 01 Sep 2005 18:48:54 +0200 |
wenzelm |
added curried_lookup/update operations -- in preparation of currying plain lookup/update;
|
changeset |
files
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
changeset |
files
|
| Thu, 01 Sep 2005 16:19:02 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 01 Sep 2005 15:58:11 +0200 |
wenzelm |
renamed 'thms_containing' to 'find_theorems' -- keep old version for the time being;
|
changeset |
files
|
| Thu, 01 Sep 2005 15:58:10 +0200 |
wenzelm |
removed obsolete 'symbols' mode;
|
changeset |
files
|
| Thu, 01 Sep 2005 15:58:08 +0200 |
wenzelm |
added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
|
changeset |
files
|
| Thu, 01 Sep 2005 11:45:54 +0200 |
paulson |
improved formatting
|
changeset |
files
|
| Thu, 01 Sep 2005 00:46:14 +0200 |
wenzelm |
isamarkuptext/txt: \par before changing sizes prevents spacing anomaly;
|
changeset |
files
|
| Thu, 01 Sep 2005 00:45:24 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 31 Aug 2005 18:46:56 +0200 |
wenzelm |
fixed ins_tokentr: AList.default;
|
changeset |
files
|
| Wed, 31 Aug 2005 17:53:35 +0200 |
nipkow |
comp -> compile
|
changeset |
files
|
| Wed, 31 Aug 2005 15:47:41 +0200 |
wenzelm |
Additional BigO lemmas that require the HOL-Complex logic image;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:49 +0200 |
wenzelm |
added copy-dump option;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:48 +0200 |
wenzelm |
added line break for 'uses';
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:47 +0200 |
wenzelm |
added no_body_context;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:46 +0200 |
wenzelm |
use_dir: added copy-dump option;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:45 +0200 |
wenzelm |
present_text: Toplevel.no_body_context prevents use of wrong context in interaction;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:44 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:43 +0200 |
wenzelm |
tuned classes_arities_of;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:39 +0200 |
wenzelm |
added Avigad-Donnelly;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:38 +0200 |
wenzelm |
reactivate postfix by change of syntax;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:37 +0200 |
wenzelm |
tuned presentation;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:36 +0200 |
wenzelm |
moved lemmas that require the HOL-Complex logic image to Complex/ex/BigO_Complex.thy;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:35 +0200 |
wenzelm |
added Complex/ex/BigO_Complex.thy;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:34 +0200 |
wenzelm |
simp_implies: proper named infix;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:33 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:32 +0200 |
wenzelm |
isatool usedir: added option -C;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:31 +0200 |
wenzelm |
added option -C: copy existing document directory;
|
changeset |
files
|
| Wed, 31 Aug 2005 15:46:30 +0200 |
wenzelm |
* Delimiters of outer tokens now produce separate LaTeX macros;
|
changeset |
files
|
| Wed, 31 Aug 2005 09:37:12 +0200 |
haftmann |
introduced AList.*
|
changeset |
files
|
| Wed, 31 Aug 2005 09:01:45 +0200 |
haftmann |
better map_entry
|
changeset |
files
|
| Tue, 30 Aug 2005 21:32:10 +0200 |
schirmer |
fixed bug in record_type_abbr_tr'
|
changeset |
files
|
| Tue, 30 Aug 2005 12:47:53 +0200 |
paulson |
patterns in setsum and setprod
|
changeset |
files
|
| Mon, 29 Aug 2005 16:51:39 +0200 |
obua |
Updated import.
|
changeset |
files
|
| Mon, 29 Aug 2005 16:25:24 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Mon, 29 Aug 2005 16:18:07 +0200 |
wenzelm |
delimiter markup for verbatim tokens;
|
changeset |
files
|
| Mon, 29 Aug 2005 16:18:06 +0200 |
wenzelm |
clarify type tok, do not emit markup flag for suppressed tokens;
|
changeset |
files
|
| Mon, 29 Aug 2005 16:18:04 +0200 |
wenzelm |
use AList operations;
|
changeset |
files
|
| Mon, 29 Aug 2005 16:18:03 +0200 |
wenzelm |
cover tagged command regions;
|
changeset |
files
|
| Mon, 29 Aug 2005 16:18:02 +0200 |
wenzelm |
tune spacing where a generated theory text is included directly;
|
changeset |
files
|
| Mon, 29 Aug 2005 11:44:23 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Mon, 29 Aug 2005 10:28:17 +0200 |
wenzelm |
recover original definitions of \isactrlsub etc.;
|
changeset |
files
|
| Mon, 29 Aug 2005 08:34:24 +0200 |
haftmann |
canonical interface for 'default'
|
changeset |
files
|
| Sun, 28 Aug 2005 19:48:15 +0200 |
wenzelm |
output \<^loc> as 'loc' span;
|
changeset |
files
|
| Sun, 28 Aug 2005 19:47:24 +0200 |
wenzelm |
isatool latex -o sty;
|
changeset |
files
|
| Sun, 28 Aug 2005 19:46:49 +0200 |
wenzelm |
added 'loc';
|
changeset |
files
|
| Sun, 28 Aug 2005 19:42:19 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Sun, 28 Aug 2005 19:42:10 +0200 |
wenzelm |
ASCII back-quote no longer sym char;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:35:39 +0200 |
wenzelm |
added \isactrlloc;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:06:07 +0200 |
wenzelm |
* ML functions legacy_bindings and use_legacy_bindings;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:55 +0200 |
wenzelm |
avoid symbolic identifier;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:54 +0200 |
wenzelm |
added (use_)legacy_bindings;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:53 +0200 |
wenzelm |
output_basic: handle AltString token;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:52 +0200 |
wenzelm |
removed obsolete type_syn;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:51 +0200 |
wenzelm |
unskolem local vars;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:50 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:49 +0200 |
wenzelm |
added alt_string;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:48 +0200 |
wenzelm |
added AltString token (delimited by ASCII back-quotes);
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:47 +0200 |
wenzelm |
removed unused dest operation;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:46 +0200 |
wenzelm |
export theorems_of;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:45 +0200 |
wenzelm |
tuned some proofs;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:44 +0200 |
wenzelm |
removed obsolete arities;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:43 +0200 |
wenzelm |
tuned size of included graph;
|
changeset |
files
|
| Sun, 28 Aug 2005 16:04:42 +0200 |
wenzelm |
added \isachardoublequoteopen/close, \isacharbackquoteopen/close;
|
changeset |
files
|
| Sun, 28 Aug 2005 10:08:36 +0200 |
haftmann |
(branch cleanup)
|
changeset |
files
|
| Sun, 28 Aug 2005 10:05:03 +0200 |
haftmann |
(allocating new branch)
|
changeset |
files
|
| Sun, 28 Aug 2005 09:36:18 +0200 |
haftmann |
added superclasses, class_le_path
|
changeset |
files
|
| Sun, 28 Aug 2005 09:26:22 +0200 |
haftmann |
added alist.ML
|
changeset |
files
|
| Sun, 28 Aug 2005 09:18:22 +0200 |
haftmann |
added 'these', removed assoc2
|
changeset |
files
|
| Sun, 28 Aug 2005 09:02:42 +0200 |
haftmann |
added alist module
|
changeset |
files
|
| Fri, 26 Aug 2005 19:47:23 +0200 |
berghofe |
Fixed bug.
|
changeset |
files
|
| Fri, 26 Aug 2005 19:36:07 +0200 |
quigley |
DFG output now works for untyped rules (ML "ResClause.untyped();")
|
changeset |
files
|
| Fri, 26 Aug 2005 10:01:06 +0200 |
ballarin |
Lemmas on dvd, power and finite summation added or strengthened.
|
changeset |
files
|
| Fri, 26 Aug 2005 08:42:52 +0200 |
haftmann |
replaced '?' by '??'
|
changeset |
files
|
| Thu, 25 Aug 2005 17:51:11 +0200 |
berghofe |
Adapted to new code generator syntax.
|
changeset |
files
|
| Thu, 25 Aug 2005 16:17:40 +0200 |
berghofe |
Put quotation marks around some occurrences of "file", since it is now
|
changeset |
files
|
| Thu, 25 Aug 2005 16:13:09 +0200 |
berghofe |
Adapted to new code generator syntax.
|
changeset |
files
|
| Thu, 25 Aug 2005 16:10:16 +0200 |
berghofe |
Implemented incremental code generation.
|
changeset |
files
|
| Thu, 25 Aug 2005 09:29:05 +0200 |
haftmann |
fixed typo
|
changeset |
files
|
| Thu, 25 Aug 2005 09:25:03 +0200 |
haftmann |
add_locale_context(_i) now exporting elements (still some refinements to be done)
|
changeset |
files
|
| Thu, 25 Aug 2005 09:23:40 +0200 |
haftmann |
added ? combinator for conditional transformations
|
changeset |
files
|
| Thu, 25 Aug 2005 09:23:13 +0200 |
haftmann |
added 'default' function
|
changeset |
files
|
| Wed, 24 Aug 2005 12:07:00 +0200 |
ballarin |
Printing of interpretations: option to show witness theorems;
|
changeset |
files
|
| Wed, 24 Aug 2005 12:05:48 +0200 |
ballarin |
Interpretation in locales: extended back end;
|
changeset |
files
|
| Tue, 23 Aug 2005 09:18:44 +0200 |
haftmann |
replaced ? by ??
|
changeset |
files
|
| Fri, 19 Aug 2005 23:20:50 +0200 |
wenzelm |
fixed deps;
|
changeset |
files
|
| Fri, 19 Aug 2005 22:50:20 +0200 |
wenzelm |
tuned arrangement of generated stuff;
|
changeset |
files
|
| Fri, 19 Aug 2005 22:44:36 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 19 Aug 2005 22:44:01 +0200 |
wenzelm |
tuned generated stuff;
|
changeset |
files
|
| Fri, 19 Aug 2005 22:28:23 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 19 Aug 2005 22:28:23 +0200 |
wenzelm |
updated;
|
changeset |
files
|