2018-04-19 |
Christian Urban |
updated to Isabelle 2016-1
default
|
file |
diff |
annotate
|
2016-03-19 |
Christian Urban |
updated to Isabelle 2016
Nominal2-Isabelle2016
|
file |
diff |
annotate
|
2015-07-09 |
Christian Urban |
updated for Isabelle 2015
|
file |
diff |
annotate
|
2014-05-19 |
Christian Urban |
changed nominal_primrec into the more appropriate nominal_function
|
file |
diff |
annotate
|
2014-05-19 |
Christian Urban |
changes from upstream
|
file |
diff |
annotate
|
2014-05-16 |
Christian Urban |
updated changes from upstream (AFP)
|
file |
diff |
annotate
|
2014-03-24 |
Christian Urban |
updated to massive changes in Isabelle
|
file |
diff |
annotate
|
2014-01-11 |
Christian Urban |
updated with current AFP version
|
file |
diff |
annotate
|
2012-10-29 |
Christian Urban |
adapted to latest change of Markus on the function package
|
file |
diff |
annotate
|
2012-06-18 |
Christian Urban |
used ML-antiquotation command_spec for new commands
|
file |
diff |
annotate
|
2012-04-30 |
Christian Urban |
adapted to change by Markus on function.ML
|
file |
diff |
annotate
|
2012-03-20 |
Christian Urban |
updated to new Isabelle (20 March)
|
file |
diff |
annotate
|
2011-11-03 |
Christian Urban |
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
|
file |
diff |
annotate
|
2011-08-28 |
Christian Urban |
updated to Isabelle 28 Aug
|
file |
diff |
annotate
|
2011-08-17 |
Christian Urban |
made same changes as in main branch
|
file |
diff |
annotate
|
2011-08-15 |
Christian Urban |
uodated to new Isabelle (15. Aug)
|
file |
diff |
annotate
|
2011-07-19 |
Christian Urban |
generated the partial eqvt-theorem for functions
|
file |
diff |
annotate
|
2011-07-18 |
Christian Urban |
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
|
file |
diff |
annotate
|
2011-06-16 |
Christian Urban |
added eqvt_at and invariant for boths sides of the equations
|
file |
diff |
annotate
|
2011-06-16 |
Christian Urban |
added a test that every function must be of pt-sort
|
file |
diff |
annotate
|
2011-06-07 |
Christian Urban |
fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
|
file |
diff |
annotate
|
2011-06-05 |
Christian Urban |
added an option for an invariant (at the moment only a stub)
|
file |
diff |
annotate
|
2011-05-30 |
Christian Urban |
functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
|
file |
diff |
annotate
|
2011-04-06 |
Christian Urban |
changed default preprocessor that does not catch variables only occuring on the right
|
file |
diff |
annotate
|
2011-03-16 |
Christian Urban |
ported changes from function package....needs Isabelle 16 March or above
|
file |
diff |
annotate
|
2011-01-17 |
Christian Urban |
exported nominal function code to external file
|
file |
diff |
annotate
|