| 2010-06-14 |
Cezary Kaliszyk |
qpaper/unfold the ball_reg_right statement
|
file |
diff |
annotate
|
| 2010-06-14 |
Christian Urban |
some tuning and start work on section 4
|
file |
diff |
annotate
|
| 2010-06-14 |
Christian Urban |
completed proof and started section about respectfulness and preservation
|
file |
diff |
annotate
|
| 2010-06-13 |
Christian Urban |
something about the quotient ype definitions
|
file |
diff |
annotate
|
| 2010-06-11 |
Christian Urban |
more on the qpaper
|
file |
diff |
annotate
|
| 2010-05-27 |
Cezary Kaliszyk |
qpaper / a bit about prs
|
file |
diff |
annotate
|
| 2010-05-26 |
Cezary Kaliszyk |
qpaper
|
file |
diff |
annotate
|
| 2010-05-26 |
Cezary Kaliszyk |
Name some respectfullness
|
file |
diff |
annotate
|
| 2010-05-10 |
Cezary Kaliszyk |
Synchronize FSet with repository
|
file |
diff |
annotate
|
| 2010-04-26 |
Cezary Kaliszyk |
merge ???
|
file |
diff |
annotate
|
| 2010-04-21 |
Cezary Kaliszyk |
infix for In
|
file |
diff |
annotate
|
| 2010-04-23 |
Cezary Kaliszyk |
Further cleaning of proofs in FSet
|
file |
diff |
annotate
|
| 2010-04-22 |
Cezary Kaliszyk |
Converted 'thm' to a lemma.
|
file |
diff |
annotate
|
| 2010-04-22 |
Cezary Kaliszyk |
Moved working Fset3 properties to FSet.
|
file |
diff |
annotate
|
| 2010-04-21 |
Cezary Kaliszyk |
append_rsp2 + isarification
|
file |
diff |
annotate
|
| 2010-04-21 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| 2010-04-21 |
Christian Urban |
removed a sorry
|
file |
diff |
annotate
|
| 2010-04-21 |
Cezary Kaliszyk |
Reorder FSet
|
file |
diff |
annotate
|
| 2010-04-21 |
Cezary Kaliszyk |
lattice properties.
|
file |
diff |
annotate
|
| 2010-04-20 |
Cezary Kaliszyk |
fsets are distributive lattices.
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
FSet is a semi-lattice
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
Putting FSet in bot typeclass.
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
reorder
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
sub_list definition and respects
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
Alternate list_eq and equivalence
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
Some new lemmas
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
More cleaning
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
remove more metis
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
more metis cleaning
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
Getting rid of 'metis'.
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
Remove 'defer'.
|
file |
diff |
annotate
|
| 2010-04-19 |
Cezary Kaliszyk |
2 more lifted lemmas needed for second representation
|
file |
diff |
annotate
|
| 2010-04-15 |
Christian Urban |
some tuning of proofs
|
file |
diff |
annotate
|
| 2010-04-14 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| 2010-04-14 |
Cezary Kaliszyk |
merge part: delete_rsp
|
file |
diff |
annotate
|
| 2010-04-14 |
Cezary Kaliszyk |
merge part1: none_memb_nil
|
file |
diff |
annotate
|
| 2010-04-14 |
Christian Urban |
added header and more tuning
|
file |
diff |
annotate
|
| 2010-04-14 |
Christian Urban |
more tuning
|
file |
diff |
annotate
|
| 2010-04-14 |
Christian Urban |
tuned
|
file |
diff |
annotate
|
| 2010-04-13 |
Cezary Kaliszyk |
Working FSet with additional lemmas.
|
file |
diff |
annotate
|
| 2010-04-13 |
Cezary Kaliszyk |
Much more in FSet (currently non-working)
|
file |
diff |
annotate
|
| 2010-04-12 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| 2010-04-12 |
Christian Urban |
some small tunings (incompleted work in Lambda.thy)
|
file |
diff |
annotate
|
| 2010-04-12 |
Cezary Kaliszyk |
Porting lemmas from Quotient package FSet to new FSet.
|
file |
diff |
annotate
|
| 2010-03-27 |
Cezary Kaliszyk |
Remove list_eq notation.
|
file |
diff |
annotate
|
| 2010-03-19 |
Cezary Kaliszyk |
A few more theorems in FSet.
|
file |
diff |
annotate
|
| 2010-03-18 |
Cezary Kaliszyk |
Added a cleaned version of FSet.
|
file |
diff |
annotate
|