Fri, 27 May 2016 20:23:55 +0200 | wenzelm | tuned proofs, to allow unfold_abs_def; | file | diff | annotate |
Thu, 28 Apr 2016 09:43:11 +0200 | wenzelm | support 'assumes' in specifications, e.g. 'definition', 'inductive'; | file | diff | annotate |
Mon, 18 Apr 2016 11:02:07 +0200 | wenzelm | avoid clash with function called "x"; | file | diff | annotate |