| Mon, 04 Jan 2010 22:16:48 +0100 |
wenzelm |
discontinued old ISABELLE and ISATOOL environment settings;
|
changeset |
files
|
| Mon, 04 Jan 2010 21:49:47 +0100 |
wenzelm |
shell functions "isabelle-process" and "isabelle" refer to the proper executables statically -- for interactive use or sloppy bash scripts;
|
changeset |
files
|
| Mon, 04 Jan 2010 20:25:56 +0100 |
wenzelm |
removed further remains of mutable theory data (cf. 25bd3ed2ac9f);
|
changeset |
files
|
| Mon, 04 Jan 2010 19:44:46 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 04 Jan 2010 16:00:24 +0100 |
haftmann |
code cache only persists on equal theories
|
changeset |
files
|
| Mon, 04 Jan 2010 16:00:23 +0100 |
haftmann |
moved name duplicates to end of theory; reduced warning noise
|
changeset |
files
|
| Mon, 04 Jan 2010 14:10:13 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 04 Jan 2010 14:09:58 +0100 |
haftmann |
modernized
|
changeset |
files
|
| Mon, 04 Jan 2010 14:09:57 +0100 |
haftmann |
added applify combinator
|
changeset |
files
|
| Mon, 04 Jan 2010 14:09:57 +0100 |
haftmann |
dropped redundant name declarations
|
changeset |
files
|
| Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
dropped copy operation for legacy TheoryDataFun
|
changeset |
files
|
| Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
code cache without copy; tuned
|
changeset |
files
|
| Mon, 04 Jan 2010 19:43:59 +0100 |
wenzelm |
report keywords as singleton messages, control message kind via print mode;
|
changeset |
files
|
| Mon, 04 Jan 2010 18:56:36 +0100 |
wenzelm |
explicit markup of document assigment message (simplified variant of earlier "edits" 8c3e1f73953d);
|
changeset |
files
|
| Mon, 04 Jan 2010 18:55:32 +0100 |
wenzelm |
omit useless (?) scaladoc;
|
changeset |
files
|
| Mon, 04 Jan 2010 18:54:22 +0100 |
wenzelm |
added Future.promise -- essentially a single-assignment variable with signalling, using the Future interface;
|
changeset |
files
|
| Mon, 04 Jan 2010 15:35:53 +0100 |
wenzelm |
after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;
|
changeset |
files
|
| Mon, 04 Jan 2010 11:55:23 +0100 |
wenzelm |
discontinued special HOL_USEDIR_OPTIONS;
|
changeset |
files
|
| Sun, 03 Jan 2010 15:09:02 +0100 |
wenzelm |
updated stats;
|
changeset |
files
|
| Sun, 03 Jan 2010 15:08:17 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Sun, 03 Jan 2010 11:03:22 +0000 |
paulson |
merged
|
changeset |
files
|
| Sun, 03 Jan 2010 11:03:00 +0000 |
paulson |
removed legacy asm_lr_simp_tac
|
changeset |
files
|
| Sun, 03 Jan 2010 10:01:23 +0100 |
nipkow |
removed more asm_rl's - unfortunately slowdown of 1 min.
|
changeset |
files
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
new year's resolution: reindented code in function package
|
changeset |
files
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
provide simp and induct rules in Function.info
|
changeset |
files
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
more official data record Function.info
|
changeset |
files
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
simplified
|
changeset |
files
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
absorb structures Decompose and Descent into Termination, to simplify further restructuring
|
changeset |
files
|
| Sat, 02 Jan 2010 22:57:19 +0100 |
nipkow |
another legacy "asm_lr"
|
changeset |
files
|
| Sat, 02 Jan 2010 21:31:33 +0100 |
nipkow |
merged
|
changeset |
files
|
| Sat, 02 Jan 2010 21:31:15 +0100 |
nipkow |
removed legacy asm_lr
|
changeset |
files
|
| Sat, 02 Jan 2010 20:10:21 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 01 Jan 2010 19:15:43 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Fri, 01 Jan 2010 17:21:44 +0100 |
nipkow |
added lemma
|
changeset |
files
|
| Fri, 01 Jan 2010 16:34:51 +0100 |
nipkow |
removed FIXME
|
changeset |
files
|
| Sat, 02 Jan 2010 20:08:04 +0100 |
wenzelm |
tuned error handling;
|
changeset |
files
|
| Sat, 02 Jan 2010 01:14:49 +0100 |
wenzelm |
Standard_System.raw_execute: optional cwd;
|
changeset |
files
|
| Sat, 02 Jan 2010 00:08:47 +0100 |
wenzelm |
Download URLs -- with progress monitor.
|
changeset |
files
|
| Fri, 01 Jan 2010 21:26:02 +0100 |
wenzelm |
Future values -- Scala version.
|
changeset |
files
|
| Thu, 31 Dec 2009 23:47:09 +0100 |
wenzelm |
added simple dialogs;
|
changeset |
files
|
| Thu, 31 Dec 2009 00:35:54 +0100 |
wenzelm |
added is_ready;
|
changeset |
files
|
| Wed, 30 Dec 2009 22:56:46 +0100 |
wenzelm |
simplified init message -- removed redundant session property;
|
changeset |
files
|
| Wed, 30 Dec 2009 22:29:37 +0100 |
wenzelm |
removed obsolete version check -- sanity delegated to Isabelle_System;
|
changeset |
files
|
| Wed, 30 Dec 2009 21:32:25 +0100 |
wenzelm |
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
|
changeset |
files
|
| Wed, 30 Dec 2009 20:25:35 +0100 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Wed, 30 Dec 2009 13:05:00 +0100 |
wenzelm |
less ambitious isatest for SML/NJ;
|
changeset |
files
|
| Wed, 30 Dec 2009 10:24:53 +0100 |
krauss |
killed a few warnings
|
changeset |
files
|
| Wed, 30 Dec 2009 01:08:33 +0100 |
krauss |
more regular axiom of infinity, with no (indirect) reference to overloaded constants
|
changeset |
files
|
| Tue, 29 Dec 2009 20:59:47 +0100 |
wenzelm |
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
|
changeset |
files
|
| Tue, 29 Dec 2009 20:30:40 +0100 |
wenzelm |
removed slightly odd Isar_Document.init;
|
changeset |
files
|
| Tue, 29 Dec 2009 16:20:39 +0100 |
wenzelm |
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
|
changeset |
files
|
| Mon, 28 Dec 2009 23:34:36 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 28 Dec 2009 22:58:25 +0100 |
wenzelm |
crude Cygwin.setup;
|
changeset |
files
|
| Mon, 28 Dec 2009 22:57:37 +0100 |
wenzelm |
ignore undefined environment;
|
changeset |
files
|
| Mon, 28 Dec 2009 22:03:14 +0100 |
wenzelm |
separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
|
changeset |
files
|
| Mon, 28 Dec 2009 20:24:09 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 28 Dec 2009 20:01:43 +0100 |
wenzelm |
system shutdown hook: strict kill;
|
changeset |
files
|
| Mon, 28 Dec 2009 18:40:13 +0100 |
wenzelm |
moved Library.decode_permissive_utf8 to Isabelle_System;
|
changeset |
files
|
| Mon, 28 Dec 2009 18:37:11 +0100 |
wenzelm |
pid without newline -- required for Scala version of system_out;
|
changeset |
files
|
| Mon, 28 Dec 2009 16:45:01 +0100 |
wenzelm |
higher-order treatment of temporary files;
|
changeset |
files
|
| Mon, 28 Dec 2009 16:24:19 +0100 |
wenzelm |
isabelle_tool: apply platform_path only once;
|
changeset |
files
|
| Mon, 28 Dec 2009 14:51:03 +0100 |
wenzelm |
slightly more paranoid cleanup of process (cf. http://kylecartmell.com/?p=9 "Five Common java.lang.Process Pitfalls");
|
changeset |
files
|
| Mon, 28 Dec 2009 13:40:30 +0100 |
wenzelm |
some sanity checks for symbol interpretation;
|
changeset |
files
|
| Sun, 27 Dec 2009 23:10:03 +0100 |
wenzelm |
allow UTF-8 in theory and file names;
|
changeset |
files
|
| Sun, 27 Dec 2009 23:09:16 +0100 |
wenzelm |
factored-out Library.decode_permissive_utf8;
|
changeset |
files
|
| Sun, 27 Dec 2009 22:36:47 +0100 |
wenzelm |
read header by scanning/parsing file;
|
changeset |
files
|
| Sun, 27 Dec 2009 22:16:41 +0100 |
wenzelm |
quoted_content: handle escapes;
|
changeset |
files
|
| Sun, 27 Dec 2009 21:34:23 +0100 |
wenzelm |
scan: operate on file (via Scan.byte_reader), more robust exception handling;
|
changeset |
files
|
| Sun, 27 Dec 2009 21:33:35 +0100 |
wenzelm |
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
|
changeset |
files
|
| Sun, 27 Dec 2009 21:30:54 +0100 |
wenzelm |
removed unused read_file;
|
changeset |
files
|
| Thu, 24 Dec 2009 17:30:55 +0000 |
paulson |
tidied proofs
|
changeset |
files
|
| Thu, 24 Dec 2009 11:05:58 +0100 |
haftmann |
made sml/nj happy
|
changeset |
files
|
| Wed, 23 Dec 2009 17:37:42 +0100 |
boehmes |
updated certificates
|
changeset |
files
|
| Wed, 23 Dec 2009 17:36:26 +0100 |
boehmes |
updated example
|
changeset |
files
|
| Wed, 23 Dec 2009 17:35:56 +0100 |
boehmes |
merged verification condition structure and term representation in one datatype,
|
changeset |
files
|
| Wed, 23 Dec 2009 11:33:01 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 23 Dec 2009 11:32:40 +0100 |
haftmann |
updated generated document sources
|
changeset |
files
|
| Wed, 23 Dec 2009 11:32:08 +0100 |
haftmann |
take care for destructive print mode properly using dedicated pretty builders
|
changeset |
files
|
| Wed, 23 Dec 2009 10:41:13 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 23 Dec 2009 10:09:06 +0100 |
haftmann |
made sml/nj happy
|
changeset |
files
|
| Wed, 23 Dec 2009 08:31:33 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 23 Dec 2009 08:31:15 +0100 |
haftmann |
dropped junk
|
changeset |
files
|
| Wed, 23 Dec 2009 08:31:15 +0100 |
haftmann |
reduced code generator cache to the baremost minimum
|
changeset |
files
|
| Wed, 23 Dec 2009 08:31:14 +0100 |
haftmann |
updated documentation
|
changeset |
files
|
| Wed, 23 Dec 2009 08:31:14 +0100 |
haftmann |
updated generated examples
|
changeset |
files
|
| Wed, 23 Dec 2009 08:31:14 +0100 |
haftmann |
reduced code generator cache to the baremost minimum; corrected spelling
|
changeset |
files
|
| Tue, 22 Dec 2009 21:48:17 +0100 |
wenzelm |
basic setup for header scanning/parsing;
|
changeset |
files
|
| Tue, 22 Dec 2009 21:47:27 +0100 |
wenzelm |
clarified atom parser: return content;
|
changeset |
files
|
| Tue, 22 Dec 2009 21:46:41 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 22 Dec 2009 19:38:06 +0100 |
wenzelm |
renamed class Outer_Keyword to Outer_Syntax;
|
changeset |
files
|
| Tue, 22 Dec 2009 18:36:01 +0100 |
wenzelm |
Isabelle session manager -- most basic setup;
|
changeset |
files
|
| Tue, 22 Dec 2009 17:59:59 +0100 |
wenzelm |
actually closer file reader;
|
changeset |
files
|
| Tue, 22 Dec 2009 17:25:41 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 22 Dec 2009 17:13:43 +0100 |
wenzelm |
added plain read_file;
|
changeset |
files
|
| Tue, 22 Dec 2009 17:13:18 +0100 |
wenzelm |
consider proper input only;
|
changeset |
files
|
| Tue, 22 Dec 2009 15:31:02 +0100 |
wenzelm |
added completion -- lazy avoids excessive table building;
|
changeset |
files
|
| Tue, 22 Dec 2009 15:00:43 +0100 |
wenzelm |
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
|
changeset |
files
|
| Tue, 22 Dec 2009 15:00:03 +0100 |
wenzelm |
class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;
|
changeset |
files
|
| Tue, 22 Dec 2009 14:58:13 +0100 |
wenzelm |
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
|
changeset |
files
|
| Mon, 21 Dec 2009 16:50:28 +0000 |
paulson |
Changes in generated code, apparently caused by changes to the code generation system itself.
|
changeset |
files
|
| Mon, 21 Dec 2009 16:49:04 +0000 |
paulson |
Polishing up the English
|
changeset |
files
|
| Mon, 21 Dec 2009 10:40:14 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 21 Dec 2009 08:32:22 +0100 |
haftmann |
merged
|
changeset |
files
|
| Mon, 21 Dec 2009 08:32:04 +0100 |
haftmann |
clarified various user-defined syntax issues
|
changeset |
files
|
| Mon, 21 Dec 2009 08:32:04 +0100 |
haftmann |
prefer prefix "iso" over potentially misleading "is"; tuned
|
changeset |
files
|
| Mon, 21 Dec 2009 08:32:03 +0100 |
haftmann |
moved lemmas o_eq_dest, o_eq_elim here
|
changeset |
files
|
| Sat, 19 Dec 2009 09:07:04 -0800 |
huffman |
add 'morphisms' option to domain_isomorphism command
|
changeset |
files
|
| Sat, 19 Dec 2009 06:07:33 -0800 |
huffman |
merged
|
changeset |
files
|
| Fri, 18 Dec 2009 20:13:23 -0800 |
huffman |
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
|
changeset |
files
|
| Fri, 18 Dec 2009 19:00:11 -0800 |
huffman |
rename equals_zero_I to minus_unique (keep old name too)
|
changeset |
files
|
| Fri, 18 Dec 2009 18:48:27 -0800 |
huffman |
add lemma swap_triple
|
changeset |
files
|
| Sun, 20 Dec 2009 18:02:13 +0100 |
wenzelm |
improve performance by reordering of parser combinators;
|
changeset |
files
|
| Sun, 20 Dec 2009 17:47:59 +0100 |
wenzelm |
added nested comments;
|
changeset |
files
|
| Sun, 20 Dec 2009 15:44:29 +0100 |
wenzelm |
more Scala sources;
|
changeset |
files
|
| Sun, 20 Dec 2009 15:44:07 +0100 |
wenzelm |
simiplified result of keyword parser (again);
|
changeset |
files
|
| Sun, 20 Dec 2009 15:42:40 +0100 |
wenzelm |
simplified result of keyword and symbols parser;
|
changeset |
files
|
| Sun, 20 Dec 2009 15:42:12 +0100 |
wenzelm |
Outer lexical syntax for Isabelle/Isar -- Scala version.
|
changeset |
files
|
| Sun, 20 Dec 2009 15:41:57 +0100 |
wenzelm |
refined some Symbol operations/signatures;
|
changeset |
files
|
| Sat, 19 Dec 2009 16:51:32 +0100 |
wenzelm |
refined some Symbol operations/signatures;
|
changeset |
files
|
| Sat, 19 Dec 2009 16:02:26 +0100 |
wenzelm |
added basic library -- Scala version;
|
changeset |
files
|