Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
-50
-24
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Nominal/Ex/Lambda.thy
2011-01-18
Christian Urban
the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions
file
|
diff
|
annotate
2011-01-17
Christian Urban
added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
file
|
diff
|
annotate
2011-01-17
Christian Urban
added a few examples of functions to Lambda.thy
file
|
diff
|
annotate
2011-01-17
Christian Urban
removed old testing code from Lambda.thy
file
|
diff
|
annotate
2011-01-09
Christian Urban
solved subgoals for depth and subst function
file
|
diff
|
annotate
2011-01-06
Christian Urban
a modified function package where, as a test, True has been injected into the compatibility condictions
file
|
diff
|
annotate
2011-01-06
Christian Urban
tuned
file
|
diff
|
annotate
2010-12-31
Christian Urban
changed res keyword to set+ for restrictions; comment by a referee
file
|
diff
|
annotate
2010-12-28
Christian Urban
automated all strong induction lemmas
file
|
diff
|
annotate
2010-12-22
Christian Urban
properly exported strong exhaust theorem; cleaned up some examples
file
|
diff
|
annotate
2010-11-10
Christian Urban
adapted to changes by Florian on the quotient package and removed local fix for function package
file
|
diff
|
annotate
2010-09-29
Christian Urban
simplified exhaust proofs
file
|
diff
|
annotate
2010-09-29
Christian Urban
test with induct_schema for simpler strong_ind proofs
file
|
diff
|
annotate
2010-08-29
Christian Urban
renamed NewParser to Nominal2
file
|
diff
|
annotate
2010-08-27
Christian Urban
make copies of the "old" files
file
|
diff
|
annotate
2010-08-26
Christian Urban
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
file
|
diff
|
annotate
2010-08-25
Christian Urban
cleaned up (almost completely) the examples
file
|
diff
|
annotate
2010-08-25
Christian Urban
automatic lifting
file
|
diff
|
annotate
2010-08-25
Christian Urban
now every lemma lifts (even with type variables)
file
|
diff
|
annotate
2010-08-25
Christian Urban
can now deal with type variables in nominal datatype definitions
file
|
diff
|
annotate
2010-08-21
Christian Urban
nominal_datatypes with type variables do not work
file
|
diff
|
annotate
2010-08-21
Christian Urban
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
file
|
diff
|
annotate
2010-06-07
Christian Urban
work on transitivity proof
file
|
diff
|
annotate
2010-05-21
Cezary Kaliszyk
Match_Lam defined on Quotient Level.
file
|
diff
|
annotate
less
more
(0)
-50
-24
tip