Nominal/FSet.thy
Fri, 15 Oct 2010 15:24:19 +0900 Cezary Kaliszyk Partially merging changes from Isabelle
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)
Sat, 18 Sep 2010 06:09:43 +0800 Christian Urban updated to Isabelle Sept 16
Thu, 22 Jul 2010 08:30:50 +0200 Christian Urban updated to new Isabelle; made FSet more "quiet"
Mon, 19 Jul 2010 07:49:10 +0100 Christian Urban minor
Sun, 18 Jul 2010 19:07:05 +0100 Christian Urban minor things on the paper
Sun, 18 Jul 2010 16:06:34 +0100 Christian Urban some test with quotient
Wed, 23 Jun 2010 15:40:00 +0100 Christian Urban merged cezary's changes
Wed, 23 Jun 2010 08:49:33 +0200 Cezary Kaliszyk merge
Wed, 23 Jun 2010 08:48:38 +0200 Cezary Kaliszyk Changes for PER and list_all2 committed to Isabelle
Tue, 22 Jun 2010 13:31:42 +0100 Christian Urban cleaned up the FSet (noise was introduced by error)
Mon, 21 Jun 2010 00:36:17 +0100 Christian Urban eliminated a quot_thm flag
Wed, 16 Jun 2010 22:29:42 +0100 Christian Urban conclusion done
Tue, 15 Jun 2010 09:12:54 +0200 Cezary Kaliszyk Qpaper / Clarify the typing system and composition of quotients issue.
Mon, 14 Jun 2010 14:45:40 +0200 Cezary Kaliszyk merge
Mon, 14 Jun 2010 14:44:18 +0200 Cezary Kaliszyk qpaper/unfold the ball_reg_right statement
Mon, 14 Jun 2010 11:51:34 +0200 Christian Urban some tuning and start work on section 4
Mon, 14 Jun 2010 04:38:25 +0200 Christian Urban completed proof and started section about respectfulness and preservation
Sun, 13 Jun 2010 17:01:15 +0200 Christian Urban something about the quotient ype definitions
Fri, 11 Jun 2010 17:52:06 +0200 Christian Urban more on the qpaper
Thu, 27 May 2010 14:30:07 +0200 Cezary Kaliszyk qpaper / a bit about prs
Wed, 26 May 2010 16:56:38 +0200 Cezary Kaliszyk qpaper
Wed, 26 May 2010 16:09:09 +0200 Cezary Kaliszyk Name some respectfullness
Mon, 10 May 2010 10:22:57 +0200 Cezary Kaliszyk Synchronize FSet with repository
Mon, 26 Apr 2010 10:01:13 +0200 Cezary Kaliszyk merge ???
Wed, 21 Apr 2010 12:25:52 +0200 Cezary Kaliszyk infix for In
Fri, 23 Apr 2010 09:54:42 +0200 Cezary Kaliszyk Further cleaning of proofs in FSet
Thu, 22 Apr 2010 12:42:15 +0200 Cezary Kaliszyk Converted 'thm' to a lemma.
Thu, 22 Apr 2010 12:33:51 +0200 Cezary Kaliszyk Moved working Fset3 properties to FSet.
Wed, 21 Apr 2010 19:10:55 +0200 Cezary Kaliszyk append_rsp2 + isarification
Wed, 21 Apr 2010 10:09:07 +0200 Christian Urban merged
Wed, 21 Apr 2010 10:08:47 +0200 Christian Urban removed a sorry
Wed, 21 Apr 2010 09:48:35 +0200 Cezary Kaliszyk Reorder FSet
Wed, 21 Apr 2010 09:13:32 +0200 Cezary Kaliszyk lattice properties.
Tue, 20 Apr 2010 15:59:57 +0200 Cezary Kaliszyk fsets are distributive lattices.
Mon, 19 Apr 2010 16:19:17 +0200 Cezary Kaliszyk FSet is a semi-lattice
Mon, 19 Apr 2010 15:54:38 +0200 Cezary Kaliszyk Putting FSet in bot typeclass.
Mon, 19 Apr 2010 15:33:19 +0200 Cezary Kaliszyk reorder
Mon, 19 Apr 2010 15:28:57 +0200 Cezary Kaliszyk sub_list definition and respects
Mon, 19 Apr 2010 15:08:29 +0200 Cezary Kaliszyk Alternate list_eq and equivalence
Mon, 19 Apr 2010 14:08:01 +0200 Cezary Kaliszyk Some new lemmas
Mon, 19 Apr 2010 13:58:10 +0200 Cezary Kaliszyk More cleaning
Mon, 19 Apr 2010 12:28:48 +0200 Cezary Kaliszyk remove more metis
Mon, 19 Apr 2010 12:20:18 +0200 Cezary Kaliszyk more metis cleaning
Mon, 19 Apr 2010 11:55:12 +0200 Cezary Kaliszyk Getting rid of 'metis'.
Mon, 19 Apr 2010 11:32:33 +0200 Cezary Kaliszyk Remove 'defer'.
Mon, 19 Apr 2010 11:04:31 +0200 Cezary Kaliszyk 2 more lifted lemmas needed for second representation
Thu, 15 Apr 2010 21:56:03 +0200 Christian Urban some tuning of proofs
Wed, 14 Apr 2010 08:42:38 +0200 Cezary Kaliszyk merge
Wed, 14 Apr 2010 08:36:54 +0200 Cezary Kaliszyk merge part: delete_rsp
Wed, 14 Apr 2010 08:35:31 +0200 Cezary Kaliszyk merge part1: none_memb_nil
Wed, 14 Apr 2010 08:16:54 +0200 Christian Urban added header and more tuning
Wed, 14 Apr 2010 07:57:55 +0200 Christian Urban more tuning
Wed, 14 Apr 2010 07:34:03 +0200 Christian Urban tuned
Tue, 13 Apr 2010 15:59:53 +0200 Cezary Kaliszyk Working FSet with additional lemmas.
Tue, 13 Apr 2010 15:00:49 +0200 Cezary Kaliszyk Much more in FSet (currently non-working)
Tue, 13 Apr 2010 00:53:48 +0200 Christian Urban merged
Tue, 13 Apr 2010 00:53:32 +0200 Christian Urban some small tunings (incompleted work in Lambda.thy)
Mon, 12 Apr 2010 17:05:19 +0200 Cezary Kaliszyk Porting lemmas from Quotient package FSet to new FSet.
Sat, 27 Mar 2010 14:38:22 +0100 Cezary Kaliszyk Remove list_eq notation.
Fri, 19 Mar 2010 06:55:17 +0100 Cezary Kaliszyk A few more theorems in FSet.
Thu, 18 Mar 2010 18:10:20 +0100 Cezary Kaliszyk Added a cleaned version of FSet.
less more (0) tip