| 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-03-13 |
Christian Urban |
updated to Isabelle changes
|
file |
diff |
annotate
|
| 2014-01-11 |
Christian Urban |
updated with current AFP version
|
file |
diff |
annotate
|
| 2013-07-01 |
Christian Urban |
updated to ne Isabelle
|
file |
diff |
annotate
|
| 2013-06-04 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
| 2013-04-18 |
Christian Urban |
updated to simplifier changes
|
file |
diff |
annotate
|
| 2012-10-04 |
Christian Urban |
removed fork_mono flag
|
file |
diff |
annotate
|
| 2012-08-07 |
Christian Urban |
definition of an auxiliary graph in nominal-primrec definitions
|
file |
diff |
annotate
|
| 2012-01-16 |
Christian Urban |
updated to Isabelle 16 January
|
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-19 |
Cezary Kaliszyk |
Update to new Isabelle
|
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-22 |
Christian Urban |
some rudimentary infrastructure for storing data about nominal datatypes
|
file |
diff |
annotate
|
| 2011-06-16 |
Christian Urban |
added eqvt_at and invariant for boths sides of the equations
|
file |
diff |
annotate
|
| 2011-06-14 |
Christian Urban |
fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
|
file |
diff |
annotate
|
| 2011-06-07 |
Christian Urban |
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
|
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-06-01 |
Christian Urban |
hopefully final fix for ho-functions
|
file |
diff |
annotate
|
| 2011-06-01 |
Christian Urban |
first test to fix the problem with free variables
|
file |
diff |
annotate
|
| 2011-05-31 |
Christian Urban |
fixed the problem with cps-like functions
|
file |
diff |
annotate
|
| 2011-05-30 |
Christian Urban |
tuned last commit
|
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-05-26 |
Christian Urban |
updated to new Isabelle
|
file |
diff |
annotate
|
| 2011-05-10 |
Christian Urban |
updated to new Isabelle (> 9 May)
|
file |
diff |
annotate
|
| 2011-03-16 |
Christian Urban |
ported changes from function package....needs Isabelle 16 March or above
|
file |
diff |
annotate
|
| 2011-02-03 |
Christian Urban |
removed diagnostic code
|
file |
diff |
annotate
|
| 2011-01-27 |
Christian Urban |
some experiments
|
file |
diff |
annotate
|
| 2011-01-25 |
Christian Urban |
made eqvt-proof explicit in the function definitions
|
file |
diff |
annotate
|
| 2011-01-18 |
Christian Urban |
deleted diagnostic code
|
file |
diff |
annotate
|
| 2011-01-18 |
Christian Urban |
some tryes about substitution over type-schemes
|
file |
diff |
annotate
|
| 2011-01-17 |
Christian Urban |
exported nominal function code to external file
|
file |
diff |
annotate
|