wenzelm [Thu, 05 Apr 2012 10:45:53 +0200] rev 47340
tuned;
wenzelm [Wed, 04 Apr 2012 21:03:30 +0200] rev 47339
tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
wenzelm [Wed, 04 Apr 2012 17:21:39 +0200] rev 47338
proper signature constraint;
wenzelm [Wed, 04 Apr 2012 17:14:19 +0200] rev 47337
tuned comments;
wenzelm [Wed, 04 Apr 2012 14:19:47 +0200] rev 47336
separate module for prover command execution;
wenzelm [Wed, 04 Apr 2012 14:00:47 +0200] rev 47335
tuned;
huffman [Wed, 04 Apr 2012 10:38:04 +0200] rev 47334
fix typo in ML structure name
wenzelm [Wed, 04 Apr 2012 11:15:54 +0200] rev 47333
removed obsolete isar-overview manual;
sultana [Wed, 04 Apr 2012 10:04:25 +0100] rev 47332
dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
bulwahn [Wed, 04 Apr 2012 10:49:42 +0200] rev 47331
merged
bulwahn [Wed, 04 Apr 2012 10:17:54 +0200] rev 47330
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn [Wed, 04 Apr 2012 10:17:08 +0200] rev 47329
improved equality check for modes in predicate compiler
huffman [Wed, 04 Apr 2012 09:00:10 +0200] rev 47328
rename ML structure to avoid shadowing earlier name
huffman [Wed, 04 Apr 2012 07:47:42 +0200] rev 47327
add type annotations to make SML happy (cf. ec6187036495)
huffman [Tue, 03 Apr 2012 23:49:24 +0200] rev 47326
merged
huffman [Tue, 03 Apr 2012 22:31:00 +0200] rev 47325
new transfer proof method
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;
wenzelm [Tue, 03 Apr 2012 16:51:01 +0200] rev 47294
retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;
wenzelm [Tue, 03 Apr 2012 16:49:05 +0200] rev 47293
another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
wenzelm [Tue, 03 Apr 2012 16:27:32 +0200] rev 47292
export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
wenzelm [Tue, 03 Apr 2012 16:10:34 +0200] rev 47291
better drop background syntax if entity depends on parameters;
more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);
wenzelm [Tue, 03 Apr 2012 14:37:16 +0200] rev 47290
more uniform abbrev vs. define;
wenzelm [Tue, 03 Apr 2012 13:47:15 +0200] rev 47289
tuned;
wenzelm [Tue, 03 Apr 2012 11:28:21 +0200] rev 47288
clarified generic_const vs. close_schematic_term;
wenzelm [Tue, 03 Apr 2012 11:21:17 +0200] rev 47287
tuned;
wenzelm [Tue, 03 Apr 2012 10:59:20 +0200] rev 47286
more uniform theory_abbrev with const_declaration;
wenzelm [Tue, 03 Apr 2012 10:04:41 +0200] rev 47285
avoid const_declaration in aux. context (cf. locale_foundation);
wenzelm [Tue, 03 Apr 2012 09:47:20 +0200] rev 47284
clarified background_foundation vs. theory_foundation (with const_declaration);
wenzelm [Tue, 03 Apr 2012 09:41:16 +0200] rev 47283
tuned;
wenzelm [Mon, 02 Apr 2012 23:55:25 +0200] rev 47282
more general standard_declaration;
generic const declaration, which is applied to nested targets (named target only);
wenzelm [Mon, 02 Apr 2012 23:27:24 +0200] rev 47281
better restore after close_target;