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