Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
-50
-30
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Nominal/Abs.thy
2010-04-21
Christian Urban
deleted the incomplete proof about pairs of abstractions
file
|
diff
|
annotate
2010-04-21
Christian Urban
incomplete tests
file
|
diff
|
annotate
2010-04-20
Christian Urban
renamed Ex1.thy to SingleLet.thy
file
|
diff
|
annotate
2010-04-15
Christian Urban
half of the pair-abs-equivalence
file
|
diff
|
annotate
2010-04-14
Christian Urban
deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell
file
|
diff
|
annotate
2010-04-14
Christian Urban
thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples
file
|
diff
|
annotate
2010-04-11
Christian Urban
corrected imports header
file
|
diff
|
annotate
2010-04-11
Christian Urban
added eqvt rules that are more standard
file
|
diff
|
annotate
2010-04-01
Cezary Kaliszyk
Let with multiple bindings.
file
|
diff
|
annotate
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
less
more
(0)
-50
-30
tip