huffman [Tue, 03 Apr 2012 22:04:50 +0200] rev 47324
renamed Tools/transfer.ML to Tools/legacy_transfer.ML
wenzelm [Tue, 03 Apr 2012 21:39:28 +0200] rev 47323
prefer prog-prove, suppress isar-overview;
wenzelm [Tue, 03 Apr 2012 21:09:09 +0200] rev 47322
merged
wenzelm [Tue, 03 Apr 2012 20:41:13 +0200] rev 47321
merged
wenzelm [Tue, 03 Apr 2012 20:42:00 +0200] rev 47320
formal integration of "prog-prove" manual;
"main" is a reference manual;
wenzelm [Tue, 03 Apr 2012 20:37:52 +0200] rev 47319
prefer static dependencies;
huffman [Tue, 03 Apr 2012 20:56:32 +0200] rev 47318
merged
huffman [Tue, 03 Apr 2012 15:15:00 +0200] rev 47317
modernized obsolete old-style theory name with proper new-style underscore
sultana [Tue, 03 Apr 2012 17:33:22 +0100] rev 47316
removed use of CharVector in generated parser, to make SMLNJ happy
wenzelm [Tue, 03 Apr 2012 20:24:00 +0200] rev 47315
avoid duplicate PIDE markup;
tuned;
wenzelm [Tue, 03 Apr 2012 20:08:08 +0200] rev 47314
less intrusive visibility;
wenzelm [Tue, 03 Apr 2012 19:49:14 +0200] rev 47313
more robust re-import wrt. non-HHF assumptions;
wenzelm [Tue, 03 Apr 2012 19:33:46 +0200] rev 47312
consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;
wenzelm [Tue, 03 Apr 2012 18:22:14 +0200] rev 47311
close context elements via Expression.cert/read_declaration;
ensure visible context;
wenzelm [Tue, 03 Apr 2012 17:48:16 +0200] rev 47310
merged
sultana [Tue, 03 Apr 2012 16:45:44 +0100] rev 47309
added me to isatest email list
kuncar [Tue, 03 Apr 2012 16:26:48 +0200] rev 47308
new package Lifting - initial commit
huffman [Tue, 03 Apr 2012 14:09:37 +0200] rev 47307
add floor/ceiling lemmas suggested by René Thiemann
nipkow [Tue, 03 Apr 2012 08:55:06 +0200] rev 47306
made sure that " is shown in tutorial text
Christian Urban <urbanc@in.tum.de> [Mon, 02 Apr 2012 21:26:46 +0100] rev 47305
merged
Christian Urban <urbanc@in.tum.de> [Mon, 02 Apr 2012 21:26:07 +0100] rev 47304
tuned proofs
nipkow [Mon, 02 Apr 2012 20:12:19 +0200] rev 47303
merged
nipkow [Mon, 02 Apr 2012 20:12:10 +0200] rev 47302
towards showing " in the tutorial
Christian Urban <urbanc@in.tum.de> [Mon, 02 Apr 2012 18:12:53 +0100] rev 47301
tuned proof in order to avoid warning message
huffman [Mon, 02 Apr 2012 16:07:24 +0200] rev 47300
remove unnecessary qualifiers on names
huffman [Mon, 02 Apr 2012 16:06:24 +0200] rev 47299
add lemma Suc_1
berghofe [Mon, 02 Apr 2012 14:09:27 +0200] rev 47298
merged
berghofe [Mon, 02 Apr 2012 13:58:59 +0200] rev 47297
Require "For" keyword to be followed by at least one whitespace, to avoid that
identifiers starting with "For" are interpreted as traceability information
wenzelm [Tue, 03 Apr 2012 17:21:33 +0200] rev 47296
normalize defs (again, cf. 008b7858f3c0);
wenzelm [Tue, 03 Apr 2012 16:53:32 +0200] rev 47295
some context examples;