| Wed, 11 Jun 2014 14:24:23 +1000 |
Hypsubst preserves equality hypotheses
|
file | diff | annotate |
| Thu, 13 Mar 2014 07:07:07 +0100 |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file | diff | annotate |
| Tue, 13 Aug 2013 16:25:47 +0200 |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file | diff | annotate |
| Fri, 27 Jul 2012 22:23:00 +0200 |
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
|
file | diff | annotate |
| Fri, 04 Mar 2011 00:09:47 +0100 |
eliminated prems;
|
file | diff | annotate |
| Mon, 21 Feb 2011 17:43:23 +0100 |
modernized specifications;
|
file | diff | annotate |
| Mon, 13 Sep 2010 11:13:15 +0200 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| Tue, 07 Sep 2010 10:05:19 +0200 |
expand_fun_eq -> ext_iff
|
file | diff | annotate |
| Thu, 22 Apr 2010 22:01:06 +0200 |
split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
|
file | diff | annotate |