Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Nominal/FSet.thy
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
less
more
(0)
tip