Sat, 27 Feb 2010 22:52:06 +0100 wenzelm further standard instances of functor Graph;
Sat, 27 Feb 2010 22:41:22 +0100 wenzelm code simplification by inlining;
Sat, 27 Feb 2010 21:56:55 +0100 wenzelm just one copy of structure Term_Graph (in Pure);
Sat, 27 Feb 2010 21:56:05 +0100 wenzelm modernized structure Int_Graph;
Sat, 27 Feb 2010 20:57:08 +0100 wenzelm clarified @{const_name} vs. @{const_abbrev};
Sat, 27 Feb 2010 20:56:03 +0100 wenzelm clarified @{const_name} (only logical consts) vs. @{const_abbrev};
Sat, 27 Feb 2010 20:55:18 +0100 wenzelm type/const name: explicitly allow abbreviations as well;
Sat, 27 Feb 2010 20:51:51 +0100 wenzelm clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
Sat, 27 Feb 2010 13:55:03 +0100 wenzelm added at-poly-test, which is intended for performance tests of Poly/ML itself;
Sat, 27 Feb 2010 13:32:55 +0100 wenzelm more precise syntax antiquotations;
Sat, 27 Feb 2010 13:32:38 +0100 wenzelm ML antiquotations for type classes;
Sat, 27 Feb 2010 13:32:18 +0100 wenzelm read_class: perform actual read, with source position;
Sat, 27 Feb 2010 13:32:05 +0100 wenzelm parallel brute-force disambiguation;
Sat, 27 Feb 2010 13:31:55 +0100 wenzelm degrade gracefully in CRITICAL section;
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip