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/Ex/AuxNoFCB.thy
2014-05-19
Christian Urban
changed nominal_primrec to nominal_function and termination to nominal_termination
file
|
diff
|
annotate
2014-05-19
Christian Urban
changed nominal_primrec into the more appropriate nominal_function
file
|
diff
|
annotate
2012-04-02
Cezary Kaliszyk
remove smt calls
file
|
diff
|
annotate
2012-03-30
Cezary Kaliszyk
More cleaning
file
|
diff
|
annotate
2012-03-30
Cezary Kaliszyk
Clean the proof of Aux
file
|
diff
|
annotate
2012-03-30
Cezary Kaliszyk
Finish all subgoals about Aux.
file
|
diff
|
annotate
2012-03-30
Cezary Kaliszyk
More on Aux
file
|
diff
|
annotate
2012-03-30
Cezary Kaliszyk
Close some of the obvious subgoals in Aux
file
|
diff
|
annotate
2012-03-30
Cezary Kaliszyk
Correct Aux and proof sketch that it's same as alpha-equality, following Dan Synek's proof.
file
|
diff
|
annotate
2012-03-29
Cezary Kaliszyk
Induction for Aux
file
|
diff
|
annotate
2012-03-29
Cezary Kaliszyk
Change definition of Aux to include alpha-convertibility for non-closed terms.
file
|
diff
|
annotate
2012-03-27
Cezary Kaliszyk
Define 'aux'
file
|
diff
|
annotate
less
more
(0)
tip