wenzelm [Sun, 27 Dec 2009 23:09:16 +0100] rev 34191
factored-out Library.decode_permissive_utf8;
wenzelm [Sun, 27 Dec 2009 22:36:47 +0100] rev 34190
read header by scanning/parsing file;
wenzelm [Sun, 27 Dec 2009 22:16:41 +0100] rev 34189
quoted_content: handle escapes;
wenzelm [Sun, 27 Dec 2009 21:34:23 +0100] rev 34188
scan: operate on file (via Scan.byte_reader), more robust exception handling;
wenzelm [Sun, 27 Dec 2009 21:33:35 +0100] rev 34187
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm [Sun, 27 Dec 2009 21:30:54 +0100] rev 34186
removed unused read_file;
paulson [Thu, 24 Dec 2009 17:30:55 +0000] rev 34185
tidied proofs
haftmann [Thu, 24 Dec 2009 11:05:58 +0100] rev 34184
made sml/nj happy
boehmes [Wed, 23 Dec 2009 17:37:42 +0100] rev 34183
updated certificates
boehmes [Wed, 23 Dec 2009 17:36:26 +0100] rev 34182
updated example
boehmes [Wed, 23 Dec 2009 17:35:56 +0100] rev 34181
merged verification condition structure and term representation in one datatype,
extended the set of operations on verification conditions (retrieve more information, advanced splitting of paths),
simplified discharging of verification conditions (due to improved datatype),
added variantions of commands (extract different parts of verification conditions, scan until first "hard" assertion)
haftmann [Wed, 23 Dec 2009 11:33:01 +0100] rev 34180
merged
haftmann [Wed, 23 Dec 2009 11:32:40 +0100] rev 34179
updated generated document sources
haftmann [Wed, 23 Dec 2009 11:32:08 +0100] rev 34178
take care for destructive print mode properly using dedicated pretty builders
wenzelm [Wed, 23 Dec 2009 10:41:13 +0100] rev 34177
merged
haftmann [Wed, 23 Dec 2009 10:09:06 +0100] rev 34176
made sml/nj happy
haftmann [Wed, 23 Dec 2009 08:31:33 +0100] rev 34175
merged
haftmann [Wed, 23 Dec 2009 08:31:15 +0100] rev 34174
dropped junk
haftmann [Wed, 23 Dec 2009 08:31:15 +0100] rev 34173
reduced code generator cache to the baremost minimum
haftmann [Wed, 23 Dec 2009 08:31:14 +0100] rev 34172
updated documentation
haftmann [Wed, 23 Dec 2009 08:31:14 +0100] rev 34171
updated generated examples
haftmann [Wed, 23 Dec 2009 08:31:14 +0100] rev 34170
reduced code generator cache to the baremost minimum; corrected spelling
wenzelm [Tue, 22 Dec 2009 21:48:17 +0100] rev 34169
basic setup for header scanning/parsing;
wenzelm [Tue, 22 Dec 2009 21:47:27 +0100] rev 34168
clarified atom parser: return content;
added tags parser;
wenzelm [Tue, 22 Dec 2009 21:46:41 +0100] rev 34167
tuned;
wenzelm [Tue, 22 Dec 2009 19:38:06 +0100] rev 34166
renamed class Outer_Keyword to Outer_Syntax;
renamed tokenize to scan (cf. ML version);
wenzelm [Tue, 22 Dec 2009 18:36:01 +0100] rev 34165
Isabelle session manager -- most basic setup;
wenzelm [Tue, 22 Dec 2009 17:59:59 +0100] rev 34164
actually closer file reader;
wenzelm [Tue, 22 Dec 2009 17:25:41 +0100] rev 34163
tuned;
wenzelm [Tue, 22 Dec 2009 17:13:43 +0100] rev 34162
added plain read_file;
wenzelm [Tue, 22 Dec 2009 17:13:18 +0100] rev 34161
consider proper input only;
added wrappers;
wenzelm [Tue, 22 Dec 2009 15:31:02 +0100] rev 34160
added completion -- lazy avoids excessive table building;
tuned signature;
wenzelm [Tue, 22 Dec 2009 15:00:43 +0100] rev 34159
Generic parsers for Isabelle/Isar outer syntax -- Scala version.
wenzelm [Tue, 22 Dec 2009 15:00:03 +0100] rev 34158
class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;
wenzelm [Tue, 22 Dec 2009 14:58:13 +0100] rev 34157
explicit representation of Token_Kind -- cannot really depend on runtime types due to erasure;
added Token_Reader;
tuned;
paulson [Mon, 21 Dec 2009 16:50:28 +0000] rev 34156
Changes in generated code, apparently caused by changes to the code generation system itself.
paulson [Mon, 21 Dec 2009 16:49:04 +0000] rev 34155
Polishing up the English
wenzelm [Mon, 21 Dec 2009 10:40:14 +0100] rev 34154
merged
haftmann [Mon, 21 Dec 2009 08:32:22 +0100] rev 34153
merged
haftmann [Mon, 21 Dec 2009 08:32:04 +0100] rev 34152
clarified various user-defined syntax issues
haftmann [Mon, 21 Dec 2009 08:32:04 +0100] rev 34151
prefer prefix "iso" over potentially misleading "is"; tuned
haftmann [Mon, 21 Dec 2009 08:32:03 +0100] rev 34150
moved lemmas o_eq_dest, o_eq_elim here
huffman [Sat, 19 Dec 2009 09:07:04 -0800] rev 34149
add 'morphisms' option to domain_isomorphism command
huffman [Sat, 19 Dec 2009 06:07:33 -0800] rev 34148
merged
huffman [Fri, 18 Dec 2009 20:13:23 -0800] rev 34147
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman [Fri, 18 Dec 2009 19:00:11 -0800] rev 34146
rename equals_zero_I to minus_unique (keep old name too)
huffman [Fri, 18 Dec 2009 18:48:27 -0800] rev 34145
add lemma swap_triple
wenzelm [Sun, 20 Dec 2009 18:02:13 +0100] rev 34144
improve performance by reordering of parser combinators;
wenzelm [Sun, 20 Dec 2009 17:47:59 +0100] rev 34143
added nested comments;
tuned;
wenzelm [Sun, 20 Dec 2009 15:44:29 +0100] rev 34142
more Scala sources;
wenzelm [Sun, 20 Dec 2009 15:44:07 +0100] rev 34141
simiplified result of keyword parser (again);
sort completions by plain string order;
moved Reverse to library.scala;
wenzelm [Sun, 20 Dec 2009 15:42:40 +0100] rev 34140
simplified result of keyword and symbols parser;
some support for parsing outer syntax tokens;
wenzelm [Sun, 20 Dec 2009 15:42:12 +0100] rev 34139
Outer lexical syntax for Isabelle/Isar -- Scala version.
wenzelm [Sun, 20 Dec 2009 15:41:57 +0100] rev 34138
refined some Symbol operations/signatures;
tuned;
wenzelm [Sat, 19 Dec 2009 16:51:32 +0100] rev 34137
refined some Symbol operations/signatures;
added Symbol.Matcher;
flexible Scan.Lexicon.symbols, with one/many/many1 variants;
wenzelm [Sat, 19 Dec 2009 16:02:26 +0100] rev 34136
added basic library -- Scala version;
added extra support for exceptions -- Scala version;
moved exn.ML to accompany exn.scala;
wenzelm [Sat, 19 Dec 2009 11:48:11 +0100] rev 34135
indicate final state of keywords;
added symbol scanner;
wenzelm [Sat, 19 Dec 2009 11:45:14 +0100] rev 34134
added symbol classification;
tuned;
wenzelm [Fri, 18 Dec 2009 16:52:36 +0100] rev 34133
tuned;
wenzelm [Fri, 18 Dec 2009 15:33:44 +0100] rev 34132
merged
wenzelm [Fri, 18 Dec 2009 15:32:52 +0100] rev 34131
imitate PG style;
wenzelm [Fri, 18 Dec 2009 15:14:59 +0100] rev 34130
merged
wenzelm [Fri, 18 Dec 2009 15:11:01 +0100] rev 34129
imitate PG colors;
blanchet [Fri, 18 Dec 2009 14:02:58 +0100] rev 34128
made Quickcheck take structured proof assumptions into account (like Refute and Nitpick) by default;
up to now, only Auto Quickcheck did -- the old behavior is available by passing "no_assms" as option