Fri, 26 Feb 2010 23:08:45 +0100 wenzelm gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;
Fri, 26 Feb 2010 23:07:27 +0100 wenzelm tuned;
Fri, 26 Feb 2010 23:05:47 +0100 wenzelm use simplified Syntax.escape;
Fri, 26 Feb 2010 21:43:26 +0100 wenzelm tuned hyp_subst_tac';
Fri, 26 Feb 2010 18:38:23 +0100 blanchet use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes
Fri, 26 Feb 2010 16:50:09 +0100 blanchet merged
Fri, 26 Feb 2010 16:49:46 +0100 blanchet more work on the new monotonicity stuff in Nitpick
Thu, 25 Feb 2010 16:33:39 +0100 blanchet improved precision of infinite "shallow" datatypes in Nitpick;
Thu, 25 Feb 2010 10:08:44 +0100 blanchet cosmetics
Fri, 26 Feb 2010 13:29:43 +0100 bulwahn merged
Fri, 26 Feb 2010 09:49:00 +0100 bulwahn merged
Thu, 25 Feb 2010 15:36:38 +0100 bulwahn adding no_topmost_reordering as new option to the code_pred command
Thu, 25 Feb 2010 14:01:34 +0100 bulwahn adopting Mutabelle to quickcheck reporting; improving quickcheck reporting
Thu, 25 Feb 2010 10:04:50 +0100 bulwahn added quiet option to quickcheck command
Thu, 25 Feb 2010 09:28:01 +0100 bulwahn added basic reporting of test cases to quickcheck
Fri, 26 Feb 2010 10:57:35 +0100 haftmann merged
Fri, 26 Feb 2010 10:48:21 +0100 haftmann use abstract code cerficates for bare code theorems
Fri, 26 Feb 2010 10:48:20 +0100 haftmann implement quotient_of for odl SML code generator
Fri, 26 Feb 2010 09:20:18 +0100 haftmann adjusted to cs. e4a7947e02b8
Wed, 24 Feb 2010 14:42:28 +0100 haftmann bound argument for abstype proposition
Wed, 24 Feb 2010 14:34:40 +0100 haftmann renamed theory Rational to Rat
Wed, 24 Feb 2010 14:19:54 +0100 haftmann tuned whitespace
Wed, 24 Feb 2010 14:19:54 +0100 haftmann more precise exception handler
Wed, 24 Feb 2010 14:19:53 +0100 haftmann more general case and induct rules; normalize and quotient_of; abstract code generation
Wed, 24 Feb 2010 14:19:53 +0100 haftmann crossproduct coprimality lemmas
Wed, 24 Feb 2010 14:19:53 +0100 haftmann lemma div_mult_swap, dvd_div_eq_mult, dvd_div_div_eq_mult
Wed, 24 Feb 2010 14:19:52 +0100 haftmann evaluation for abstypes
Thu, 25 Feb 2010 22:46:52 +0100 wenzelm modernized structure Split_Rule;
Thu, 25 Feb 2010 22:32:09 +0100 wenzelm more antiquotations;
Thu, 25 Feb 2010 22:17:33 +0100 wenzelm explicit @{type_syntax} markup;
Thu, 25 Feb 2010 22:15:27 +0100 wenzelm explicit @{type_syntax} markup;
Thu, 25 Feb 2010 22:08:43 +0100 wenzelm more orthogonal antiquotations for type constructors;
Thu, 25 Feb 2010 22:06:43 +0100 wenzelm clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
Thu, 25 Feb 2010 22:05:34 +0100 wenzelm provide direct access to the different kinds of type declarations;
Thu, 25 Feb 2010 09:16:16 +0100 boehmes use mixfix syntax for Boogie types
Wed, 24 Feb 2010 22:45:14 +0100 wenzelm merged
Wed, 24 Feb 2010 18:39:24 +0100 boehmes added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
Wed, 24 Feb 2010 22:09:50 +0100 wenzelm modernized syntax declarations, and make them actually work with authentic syntax;
Wed, 24 Feb 2010 22:04:10 +0100 wenzelm observe standard convention for syntax consts;
Wed, 24 Feb 2010 21:59:21 +0100 wenzelm proper type syntax (cf. 7425aece4ee3);
Wed, 24 Feb 2010 21:55:46 +0100 wenzelm observe standard convention for syntax consts;
Wed, 24 Feb 2010 20:37:01 +0100 wenzelm allow general mixfix syntax for type constructors;
Wed, 24 Feb 2010 07:06:39 -0800 huffman merged
Tue, 23 Feb 2010 14:44:43 -0800 huffman merged
Tue, 23 Feb 2010 14:44:24 -0800 huffman remove redundant lemma realpow_increasing
Tue, 23 Feb 2010 14:38:06 -0800 huffman remove redundant simp rules from RealPow.thy
Tue, 23 Feb 2010 12:35:32 -0800 huffman adapt to new realpow rules
Tue, 23 Feb 2010 11:14:09 -0800 huffman adapt to changes in simpset
Tue, 23 Feb 2010 10:37:25 -0800 huffman moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
Tue, 23 Feb 2010 07:45:54 -0800 huffman move float syntax from RealPow to Rational
Wed, 24 Feb 2010 11:55:52 +0100 blanchet compile
Wed, 24 Feb 2010 11:35:39 +0100 blanchet merged
Wed, 24 Feb 2010 11:35:10 +0100 blanchet compile
Wed, 24 Feb 2010 11:07:58 +0100 blanchet make example compile
Wed, 24 Feb 2010 09:59:54 +0100 blanchet got rid of "axclass", apparently
Wed, 24 Feb 2010 09:19:21 +0100 blanchet merged
Wed, 24 Feb 2010 09:18:31 +0100 blanchet cosmetics
Tue, 23 Feb 2010 19:10:25 +0100 blanchet support local definitions in Nitpick
Tue, 23 Feb 2010 16:53:13 +0100 blanchet show Kodkod warning message even in non-verbose mode
Tue, 23 Feb 2010 15:56:13 +0100 blanchet distinguish between Kodkodi warnings and errors in Nitpick;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip