Sun, 31 Jan 2010 14:51:32 +0100 haftmann canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
Sun, 31 Jan 2010 14:51:32 +0100 haftmann dropped some redundancies
Sun, 31 Jan 2010 14:51:31 +0100 haftmann generalized lemma foldl_apply_inv to foldl_apply
Sun, 31 Jan 2010 14:51:30 +0100 haftmann more correspondence lemmas between related operations; tuned some proofs
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Thu, 28 Jan 2010 11:48:43 +0100 haftmann dropped mk_left_commute; use interpretation of locale abel_semigroup instead
Wed, 27 Jan 2010 14:03:08 +0100 haftmann merged
Wed, 27 Jan 2010 14:02:53 +0100 haftmann a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML
Wed, 27 Jan 2010 14:02:53 +0100 haftmann lemma Image_closed_trancl
Wed, 27 Jan 2010 14:02:52 +0100 haftmann corrected type of typecopy constructor
Wed, 27 Jan 2010 14:02:52 +0100 haftmann tuned structure; moved non-related quickcheck.setup to Code_Generator.thy
Wed, 27 Jan 2010 11:47:17 +0100 berghofe Changed author; removed debugging code.
Mon, 25 Jan 2010 19:31:50 +0100 bulwahn merged
Mon, 25 Jan 2010 16:19:42 +0100 bulwahn adding Mutabelle to repository
Mon, 25 Jan 2010 16:56:24 +0100 hoelzl Replaced vec1 and dest_vec1 by abbreviation.
Fri, 22 Jan 2010 16:59:21 +0100 haftmann merged
Fri, 22 Jan 2010 16:56:51 +0100 haftmann HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
Fri, 22 Jan 2010 16:38:58 +0100 boehmes merged
Fri, 22 Jan 2010 16:38:21 +0100 boehmes support skolem constant for extensional arrays in Z3 proofs
Fri, 22 Jan 2010 16:33:44 +0100 boehmes drop underscores at end of names coming from Boogie
Fri, 22 Jan 2010 15:26:29 +0100 bulwahn merged
Fri, 22 Jan 2010 11:42:28 +0100 bulwahn correctly hiding facts of Lazy_Sequence
Thu, 21 Jan 2010 14:13:21 +0100 bulwahn corrected and simplified Spec_Rules registration in the Recdef package
Thu, 21 Jan 2010 12:20:28 +0100 bulwahn merged
Thu, 21 Jan 2010 12:18:41 +0100 bulwahn adopting predicate compiler to new Spec_Rules and eliminating the use of Nitpick_Simps
Wed, 20 Jan 2010 18:08:08 +0100 bulwahn adopting Sequences
Wed, 20 Jan 2010 18:02:22 +0100 bulwahn added registration of equational theorems from prim_rec and rec_def to Spec_Rules
Wed, 20 Jan 2010 14:09:46 +0100 bulwahn merged
Mon, 18 Jan 2010 10:34:27 +0100 krauss function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
Wed, 20 Jan 2010 14:05:17 +0100 bulwahn merged
Wed, 20 Jan 2010 11:56:45 +0100 bulwahn refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
Fri, 22 Jan 2010 13:39:00 +0100 haftmann simplified proofs
Fri, 22 Jan 2010 13:38:40 +0100 haftmann NEWS
Fri, 22 Jan 2010 13:38:29 +0100 haftmann more accurate dependencies
Fri, 22 Jan 2010 13:38:28 +0100 haftmann code literals: distinguish numeral classes by different entries
Fri, 22 Jan 2010 13:38:28 +0100 haftmann cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
Thu, 21 Jan 2010 09:27:57 +0100 haftmann merged
Sat, 16 Jan 2010 17:15:28 +0100 haftmann dropped some old primrecs and some constdefs
Sat, 16 Jan 2010 17:15:27 +0100 haftmann explicit CONST in translations
Sat, 16 Jan 2010 17:15:27 +0100 haftmann modernized syntax
Wed, 20 Jan 2010 11:54:19 +0100 blanchet fix issues with previous Nitpick change
Wed, 20 Jan 2010 10:38:19 +0100 blanchet merged
Wed, 20 Jan 2010 10:38:06 +0100 blanchet some work on Nitpick's support for quotient types;
Thu, 14 Jan 2010 17:06:35 +0100 blanchet removed the Nitpick code that loaded the "Nitpick" theory explicitly if it's not already loaded, because this didn't work properly and is of doubtful value
Tue, 19 Jan 2010 17:53:11 +0100 hoelzl Added transpose_rectangle, when the input list is rectangular.
Tue, 19 Jan 2010 16:52:01 +0100 hoelzl Add transpose to the List-theory.
Tue, 02 Feb 2010 21:37:27 +0100 wenzelm some examples for basic context operations;
Tue, 02 Feb 2010 13:22:36 +0100 wenzelm minimal tuning of this slightly dated material;
Tue, 02 Feb 2010 13:11:04 +0100 wenzelm added Subgoal.FOCUS;
Tue, 02 Feb 2010 12:37:57 +0100 wenzelm misc tuning and clarification;
Tue, 02 Feb 2010 11:47:49 +0100 wenzelm moved examples to proper place;
Mon, 01 Feb 2010 22:46:12 +0100 wenzelm more details on long names, binding/naming, name space;
Sun, 31 Jan 2010 22:08:25 +0100 wenzelm Variable.names_of;
Sun, 31 Jan 2010 21:40:44 +0100 wenzelm more details on Isabelle symbols;
Fri, 29 Jan 2010 23:59:03 +0100 wenzelm theory data example;
Fri, 29 Jan 2010 23:57:57 +0100 wenzelm basic setup for ML examples: tag "mlex";
Thu, 28 Jan 2010 22:39:48 +0100 wenzelm tuned signature;
Thu, 28 Jan 2010 22:38:11 +0100 wenzelm formal markup of type aliases;
Thu, 28 Jan 2010 22:19:27 +0100 wenzelm make underscores visually appear as such, although TeX-nically they are just rules (e.g. cannot be searched);
Sat, 16 Jan 2010 21:14:15 +0100 wenzelm Netbeans Library "Scala-compiler";
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip