Mon, 18 Oct 2010 14:13:28 +0900 Cezary Kaliszyk Use the generalized compositional quotient theorem
Sun, 17 Oct 2010 21:40:23 +0100 Christian Urban fixed typo
Sun, 17 Oct 2010 15:53:37 +0100 Christian Urban all tests work again
Sun, 17 Oct 2010 15:28:05 +0100 Christian Urban some tuning
Sun, 17 Oct 2010 13:35:52 +0100 Christian Urban naming scheme is now *_fset (not f*_)
Fri, 15 Oct 2010 23:45:54 +0100 Christian Urban more cleaning
Fri, 15 Oct 2010 17:37:44 +0100 Christian Urban further tuning
Fri, 15 Oct 2010 16:01:03 +0100 Christian Urban renamed fminus_raw to diff_list
Fri, 15 Oct 2010 15:58:48 +0100 Christian Urban renamed fcard_raw to card_list
Fri, 15 Oct 2010 15:56:16 +0100 Christian Urban slight update
Fri, 15 Oct 2010 15:47:20 +0100 Christian Urban Further reorganisation and cleaning
Fri, 15 Oct 2010 14:11:23 +0100 Christian Urban further cleaning
Fri, 15 Oct 2010 13:28:39 +0100 Christian Urban typo
Fri, 15 Oct 2010 16:32:34 +0900 Cezary Kaliszyk FSet: stronger fact in Isabelle.
Fri, 15 Oct 2010 16:23:26 +0900 Cezary Kaliszyk FSet synchronizing
Fri, 15 Oct 2010 15:52:40 +0900 Cezary Kaliszyk Synchronizing FSet further.
Fri, 15 Oct 2010 15:24:19 +0900 Cezary Kaliszyk Partially merging changes from Isabelle
Thu, 14 Oct 2010 17:32:06 +0100 Christian Urban fixed the typo in the abstract and the problem with append (the type of map_k
Thu, 14 Oct 2010 15:58:34 +0100 Christian Urban changed format of the pearl paper
Thu, 14 Oct 2010 11:09:52 +0100 Christian Urban deleted some unused lemmas
Thu, 14 Oct 2010 04:14:22 +0100 Christian Urban major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
Wed, 13 Oct 2010 22:55:58 +0100 Christian Urban more on the pearl paper
Tue, 12 Oct 2010 13:06:18 +0100 Christian Urban added a section about abstractions
Tue, 12 Oct 2010 10:07:48 +0100 Christian Urban tiny work on the pearl paper
Fri, 08 Oct 2010 23:53:51 +0100 Christian Urban tuned
Fri, 08 Oct 2010 23:49:18 +0100 Christian Urban added apendix to paper detailing one proof
Fri, 08 Oct 2010 15:37:11 +0100 Christian Urban minor
Fri, 08 Oct 2010 15:35:14 +0100 Christian Urban minor
Fri, 08 Oct 2010 13:41:54 +0100 Christian Urban down to 20 pages
Thu, 07 Oct 2010 14:23:32 +0900 Cezary Kaliszyk minor
Wed, 06 Oct 2010 21:32:44 +0100 Christian Urban down to 21 pages and changed strong induction section
Wed, 06 Oct 2010 08:13:09 +0100 Christian Urban tuned
Wed, 06 Oct 2010 08:09:40 +0100 Christian Urban down to 22 pages
Tue, 05 Oct 2010 21:48:31 +0100 Christian Urban down to 23 pages
Tue, 05 Oct 2010 08:43:49 +0100 Christian Urban down to 24 pages and a bit
Tue, 05 Oct 2010 07:30:37 +0100 Christian Urban llncs and more sqeezing
Mon, 04 Oct 2010 12:39:57 +0100 Christian Urban first part of sqeezing everything into 20 pages (at the moment we have 26)
Mon, 04 Oct 2010 07:25:37 +0100 Christian Urban changed to llncs
Fri, 01 Oct 2010 07:11:47 -0400 Christian Urban merged
Fri, 01 Oct 2010 07:09:59 -0400 Christian Urban minor experiments
Thu, 30 Sep 2010 07:43:46 -0400 Christian Urban merged
Wed, 29 Sep 2010 16:49:13 -0400 Christian Urban simplified exhaust proofs
Fri, 01 Oct 2010 15:44:50 +0900 Cezary Kaliszyk Made the paper to compile with the renamings.
Wed, 29 Sep 2010 09:51:57 -0400 Christian Urban merged
Wed, 29 Sep 2010 09:47:26 -0400 Christian Urban worked example Foo1 with induct_schema
Wed, 29 Sep 2010 07:39:06 -0400 Christian Urban merged
Wed, 29 Sep 2010 06:45:01 -0400 Christian Urban use also induct_schema for the Let-example (permute_bn is used)
Wed, 29 Sep 2010 04:42:37 -0400 Christian Urban test with induct_schema for simpler strong_ind proofs
Wed, 29 Sep 2010 16:36:31 +0900 Cezary Kaliszyk substitution definition with 'next_name'.
Tue, 28 Sep 2010 08:21:47 -0400 Christian Urban merged
Tue, 28 Sep 2010 05:56:11 -0400 Christian Urban added Foo1 to explore a contrived example
Mon, 27 Sep 2010 12:19:17 -0400 Christian Urban added postprocessed fresh-lemmas for constructors
Mon, 27 Sep 2010 09:51:15 -0400 Christian Urban post-processed eq_iff and supp threormes according to the fv-supp equality
Mon, 27 Sep 2010 04:56:49 -0400 Christian Urban more consistent naming in Abs.thy
Mon, 27 Sep 2010 04:56:28 -0400 Christian Urban some experiments
Mon, 27 Sep 2010 04:10:36 -0400 Christian Urban added simp rules for prod_fv and prod_alpha
Sun, 26 Sep 2010 17:57:30 -0400 Christian Urban a few more words about Ott
Sat, 25 Sep 2010 08:38:04 -0400 Christian Urban lifted size_thms and exported them as <name>.size
Sat, 25 Sep 2010 08:28:45 -0400 Christian Urban cleaned up two examples
Sat, 25 Sep 2010 02:53:39 +0200 Christian Urban added example about datatypes
(0) -1000 -300 -100 -60 +60 +100 +300 tip