| Wed, 11 Jun 2014 14:24:23 +1000 |
Thomas Sewell |
Hypsubst preserves equality hypotheses
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 07:07:07 +0100 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2012 23:59:37 +0100 |
berghofe |
Replaced perm_set_eq by perm_set_def
|
file |
diff |
annotate
|
| Wed, 28 Dec 2011 20:03:13 +0100 |
wenzelm |
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
|
file |
diff |
annotate
|
| Sat, 13 Aug 2011 18:10:14 -0700 |
huffman |
HOL-Nominal-Examples: respect distinction between sets and functions
|
file |
diff |
annotate
|
| Fri, 04 Mar 2011 00:09:47 +0100 |
wenzelm |
eliminated prems;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 22:01:06 +0200 |
wenzelm |
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
|