bulwahn [Fri, 06 Nov 2009 19:02:36 +0100] rev 33491
merged
bulwahn [Fri, 06 Nov 2009 16:59:17 +0100] rev 33490
merged
bulwahn [Fri, 06 Nov 2009 14:16:57 +0100] rev 33489
merged
bulwahn [Fri, 06 Nov 2009 12:10:55 +0100] rev 33488
merge
bulwahn [Fri, 06 Nov 2009 08:47:32 +0100] rev 33487
merged
bulwahn [Fri, 06 Nov 2009 08:18:35 +0100] rev 33486
adopted the predicate compile quickcheck
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33485
made definition of functions generically for the different instances
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33484
renamed generator to random_function in the predicate compiler
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33483
improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33482
strictly respecting the line margin in the predicate compiler core
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33481
adopted mode syntax for values command
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33480
disabled upt example because of a problem due to overloaded constants with the predicate compiler
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33479
added optional mode annotations for parameters in the values command
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33478
moved values command from core to predicate compile
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33477
added further example of the values command
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33476
Adopted output of values command
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33475
improved handling of overloaded constants; examples with numerals
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33474
made SML/NJ happy; tuned
bulwahn [Fri, 06 Nov 2009 08:11:58 +0100] rev 33473
adding tracing function for evaluated code; annotated compilation in the predicate compiler
boehmes [Fri, 06 Nov 2009 17:52:57 +0100] rev 33472
added documentation for local SMT solver setup and available SMT options,
added verbose output for SMT solver invocation,
test if local SMT solver exists before invoking it,
always trace (possible) counterexamples,
documented existence of SMT server
krauss [Fri, 06 Nov 2009 14:42:42 +0100] rev 33471
renamed method induct_scheme to induction_schema
krauss [Fri, 06 Nov 2009 13:49:19 +0100] rev 33470
NEWS
krauss [Fri, 06 Nov 2009 13:42:29 +0100] rev 33469
removed session SizeChange: outdated, only half-functional, alternatives exist (cf. size_change method)
krauss [Fri, 06 Nov 2009 13:36:46 +0100] rev 33468
renamed method sizechange to size_change
krauss [Fri, 06 Nov 2009 12:13:45 +0100] rev 33467
added boehmes and hoelzl to isatest mailings
wenzelm [Fri, 06 Nov 2009 10:26:13 +0100] rev 33466
merged
boehmes [Fri, 06 Nov 2009 09:27:20 +0100] rev 33465
tuned
ballarin [Thu, 05 Nov 2009 20:42:47 +0100] rev 33464
Merged.
ballarin [Wed, 04 Nov 2009 22:54:42 +0100] rev 33463
Merged.
ballarin [Wed, 04 Nov 2009 22:51:27 +0100] rev 33462
Use PrintMode.setmp to make thread-safe; avoid code clones.
ballarin [Mon, 02 Nov 2009 22:51:22 +0100] rev 33461
Make output indenpendent of current print mode.
ballarin [Mon, 02 Nov 2009 21:27:26 +0100] rev 33460
Relax on type agreement with original context when applying term syntax.
wenzelm [Thu, 05 Nov 2009 23:59:23 +0100] rev 33459
tuned;
wenzelm [Thu, 05 Nov 2009 22:59:57 +0100] rev 33458
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
tuned signature;
tuned;
wenzelm [Thu, 05 Nov 2009 22:08:47 +0100] rev 33457
adapted LocalTheory.declaration;
wenzelm [Thu, 05 Nov 2009 22:06:46 +0100] rev 33456
allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm [Thu, 05 Nov 2009 20:44:42 +0100] rev 33455
declare Spec_Rules for most basic definitional packages;
wenzelm [Thu, 05 Nov 2009 20:41:45 +0100] rev 33454
misc tuning and clarification;
wenzelm [Thu, 05 Nov 2009 20:40:16 +0100] rev 33453
scalable version of Named_Thms, using Item_Net;
wenzelm [Thu, 05 Nov 2009 17:59:49 +0100] rev 33452
merged
wenzelm [Thu, 05 Nov 2009 17:36:15 +0100] rev 33451
merged
wenzelm [Thu, 05 Nov 2009 16:23:51 +0100] rev 33450
more accurate cleanup;
wenzelm [Thu, 05 Nov 2009 15:55:07 +0100] rev 33449
merged
wenzelm [Thu, 05 Nov 2009 15:54:14 +0100] rev 33448
more accurate dependencies;
boehmes [Thu, 05 Nov 2009 15:44:39 +0100] rev 33447
merged
boehmes [Thu, 05 Nov 2009 15:24:49 +0100] rev 33446
handle let expressions inside terms by unfolding (instead of raising an exception),
added examples to test this feature
boehmes [Thu, 05 Nov 2009 14:48:40 +0100] rev 33445
shorter names for variables and verification conditions,
auto-fix variables occurring in a verification condition
boehmes [Thu, 05 Nov 2009 14:41:37 +0100] rev 33444
added references to HOL-Boogie papers
wenzelm [Thu, 05 Nov 2009 17:58:58 +0100] rev 33443
tuned header;
use plain simultaneous lemma statements -- Pure's &&& should hardly ever occur in user space;
wenzelm [Thu, 05 Nov 2009 17:02:43 +0100] rev 33442
made SML/NJ happy;
normalized type abbreviations;
wenzelm [Thu, 05 Nov 2009 16:10:49 +0100] rev 33441
eliminated funny record patterns and made SML/NJ happy;
wenzelm [Thu, 05 Nov 2009 14:47:27 +0100] rev 33440
proper header;
eliminated SML97's opaque signature constrain, which is essentially a legacy feature (due to problems with ML toplevel pretty printing);
wenzelm [Thu, 05 Nov 2009 14:37:39 +0100] rev 33439
more accurate dependencies;
tuned;
wenzelm [Thu, 05 Nov 2009 13:57:56 +0100] rev 33438
merged
krauss [Wed, 04 Nov 2009 17:17:30 +0100] rev 33437
added Tree23 to IsaMakefile
nipkow [Wed, 04 Nov 2009 16:54:22 +0100] rev 33436
New
nipkow [Wed, 04 Nov 2009 10:17:58 +0100] rev 33435
merged
nipkow [Wed, 04 Nov 2009 10:17:43 +0100] rev 33434
fixed order of parameters in induction rules
krauss [Wed, 04 Nov 2009 09:43:25 +0100] rev 33433
added bulwahn to isatest mailings
nipkow [Wed, 04 Nov 2009 09:18:46 +0100] rev 33432
merged