Mon, 28 Jun 2010 15:23:56 +0100 |
Christian Urban |
slight cleaning
|
changeset |
files
|
Sun, 27 Jun 2010 21:41:21 +0100 |
Christian Urban |
fixed according to changes in quotient
|
changeset |
files
|
Thu, 24 Jun 2010 21:35:11 +0100 |
Christian Urban |
added definition of the quotient types
|
changeset |
files
|
Thu, 24 Jun 2010 19:32:33 +0100 |
Christian Urban |
fixed according to changes in quotient
|
changeset |
files
|
Thu, 24 Jun 2010 00:41:41 +0100 |
Christian Urban |
added comment about partial equivalence relations
|
changeset |
files
|
Thu, 24 Jun 2010 00:27:37 +0100 |
Christian Urban |
even further polishing of the qpaper
|
changeset |
files
|
Wed, 23 Jun 2010 22:41:16 +0100 |
Christian Urban |
polished paper again (and took out some claims about Homeier's package)
|
changeset |
files
|
Wed, 23 Jun 2010 15:59:43 +0100 |
Christian Urban |
some slight polishing on the paper
|
changeset |
files
|
Wed, 23 Jun 2010 15:40:00 +0100 |
Christian Urban |
merged cezary's changes
|
changeset |
files
|
Wed, 23 Jun 2010 15:21:04 +0100 |
Christian Urban |
whitespace
|
changeset |
files
|
Wed, 23 Jun 2010 09:01:45 +0200 |
Cezary Kaliszyk |
Un-do the second change to SingleLet.
|
changeset |
files
|
Wed, 23 Jun 2010 08:49:33 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Wed, 23 Jun 2010 08:48:38 +0200 |
Cezary Kaliszyk |
Changes for PER and list_all2 committed to Isabelle
|
changeset |
files
|
Fri, 18 Jun 2010 15:22:58 +0200 |
Cezary Kaliszyk |
changes for partial-equivalence quotient package
|
changeset |
files
|
Wed, 23 Jun 2010 06:54:48 +0100 |
Christian Urban |
deleted compose-lemmas in Abs (not needed anymore)
|
changeset |
files
|
Wed, 23 Jun 2010 06:45:03 +0100 |
Christian Urban |
deleted equivp_hack
|
changeset |
files
|
Tue, 22 Jun 2010 18:07:53 +0100 |
Christian Urban |
proved eqvip theorems for alphas
|
changeset |
files
|
Tue, 22 Jun 2010 13:31:42 +0100 |
Christian Urban |
cleaned up the FSet (noise was introduced by error)
|
changeset |
files
|
Tue, 22 Jun 2010 13:05:00 +0100 |
Christian Urban |
prove that alpha implies alpha_bn (needed for rsp proofs)
|
changeset |
files
|
Mon, 21 Jun 2010 15:41:59 +0100 |
Christian Urban |
further post-submission tuning
|
changeset |
files
|
Mon, 21 Jun 2010 06:47:40 +0100 |
Christian Urban |
merged with main line
|
changeset |
files
|
Mon, 21 Jun 2010 06:46:28 +0100 |
Christian Urban |
merged
|
changeset |
files
|
Fri, 11 Jun 2010 03:02:42 +0200 |
Christian Urban |
also symmetry
|
changeset |
files
|
Thu, 10 Jun 2010 14:53:45 +0200 |
Christian Urban |
merged
|
changeset |
files
|
Thu, 10 Jun 2010 14:53:28 +0200 |
Christian Urban |
premerge
|
changeset |
files
|
Wed, 09 Jun 2010 15:14:16 +0200 |
Christian Urban |
transitivity proofs done
|
changeset |
files
|
Mon, 07 Jun 2010 11:46:26 +0200 |
Christian Urban |
merged
|
changeset |
files
|
Mon, 07 Jun 2010 11:43:01 +0200 |
Christian Urban |
work on transitivity proof
|
changeset |
files
|
Thu, 03 Jun 2010 15:02:52 +0200 |
Christian Urban |
added uminus_eqvt
|
changeset |
files
|
Thu, 03 Jun 2010 11:48:44 +0200 |
Christian Urban |
fixed problem with eqvt proofs
|
changeset |
files
|