#
3241d387 |
|
06-Jun-2018 |
nipkow <none@none> |
Keep filter input syntax
|
#
e0e22efa |
|
22-May-2018 |
nipkow <none@none> |
First step to remove nonstandard "[x <- xs. P]" syntax: only input --HG-- extra : amend_source : a2e6a2312b63a5ed1947d3302e43341c073c9f03
|
#
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
#
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
c3eff356 |
|
08-Sep-2014 |
blanchet <none@none> |
improved 'datatype_compat' further for recursion through functions
|
#
aff8c6a4 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
9027a081 |
|
03-Mar-2011 |
wenzelm <none@none> |
eliminated prems;
|
#
7a4b6a89 |
|
21-Feb-2011 |
wenzelm <none@none> |
modernized specifications;
|
#
077493ab |
|
08-Sep-2010 |
haftmann <none@none> |
modernized primrec
|
#
7755f525 |
|
22-Jul-2009 |
Christian Urban <urbanc@in.tum.de> |
tuned proofs and added some lemmas
|
#
c49b40c1 |
|
21-Jan-2009 |
haftmann <none@none> |
no base sort in class import
|
#
14e04d28 |
|
13-Dec-2008 |
berghofe <none@none> |
Unified syntax of nominal_primrec with the one used by fun(ction) and new version of primrec command.
|
#
3c658208 |
|
21-Oct-2008 |
berghofe <none@none> |
Example for using the generalized version of nominal_inductive.
|
#
84287c15 |
|
04-Mar-2008 |
urbanc <none@none> |
added new example
|