Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
-30
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Nominal/Abs.thy
2010-03-29
Cezary Kaliszyk
Abs_gen and Abs_let simplifications.
file
|
diff
|
annotate
2010-03-28
Christian Urban
merged
file
|
diff
|
annotate
2010-03-28
Christian Urban
got rid of the aux-function on the raw level, by defining it with function on the quotient level
file
|
diff
|
annotate
2010-03-27
Cezary Kaliszyk
Generalize Abs_eq_iff.
file
|
diff
|
annotate
2010-03-27
Cezary Kaliszyk
New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
file
|
diff
|
annotate
2010-03-27
Cezary Kaliszyk
Removed some warnings.
file
|
diff
|
annotate
2010-03-26
Cezary Kaliszyk
merge
file
|
diff
|
annotate
2010-03-26
Cezary Kaliszyk
Modified abs_gen_sym and abs_gen_trans so it becomes usable in the proofs.
file
|
diff
|
annotate
2010-03-26
Christian Urban
more on the paper
file
|
diff
|
annotate
2010-03-26
Christian Urban
simplification
file
|
diff
|
annotate
2010-03-26
Christian Urban
merged
file
|
diff
|
annotate
2010-03-23
Christian Urban
merged
file
|
diff
|
annotate
2010-03-23
Christian Urban
more on the paper
file
|
diff
|
annotate
2010-03-23
Cezary Kaliszyk
Remove compose_eqvt
file
|
diff
|
annotate
2010-03-22
Cezary Kaliszyk
equivp_cheat can be removed for all one-permutation examples.
file
|
diff
|
annotate
2010-03-20
Christian Urban
moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp
file
|
diff
|
annotate
2010-03-20
Christian Urban
started cleaning up and introduced 3 versions of ~~gen
file
|
diff
|
annotate
2010-03-20
Christian Urban
moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas
file
|
diff
|
annotate
2010-03-19
Cezary Kaliszyk
Keep only one copy of infinite_Un.
file
|
diff
|
annotate
2010-03-19
Cezary Kaliszyk
Added a missing 'import'.
file
|
diff
|
annotate
2010-03-19
Cezary Kaliszyk
Showed the instance: fset::(at) fs
file
|
diff
|
annotate
2010-03-17
Cezary Kaliszyk
Proper compose_sym2
file
|
diff
|
annotate
2010-03-17
Cezary Kaliszyk
Trying to find a compose lemma for 2 arguments.
file
|
diff
|
annotate
2010-03-17
Christian Urban
added proof of supp/fv for type schemes
file
|
diff
|
annotate
2010-03-17
Cezary Kaliszyk
Fix for the change of alpha_gen.
file
|
diff
|
annotate
2010-03-17
Cezary Kaliszyk
merge
file
|
diff
|
annotate
2010-03-17
Cezary Kaliszyk
Lifting theorems with compound fv and compound alpha.
file
|
diff
|
annotate
2010-03-17
Christian Urban
added another supp-proof for the non-recursive case
file
|
diff
|
annotate
2010-03-16
Christian Urban
merge and proof of support for non-recursive case
file
|
diff
|
annotate
2010-03-15
Christian Urban
merged (confirmed to work with Isabelle from 6th March)
file
|
diff
|
annotate
less
more
(0)
-30
tip