| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
6f0c89b5 |
|
26-Jun-2015 |
wenzelm <none@none> |
tuned whitespace;
|
| #
03e209c5 |
|
21-Apr-2015 |
nipkow <none@none> |
added simp rules for ==>
|
| #
9fd71573 |
|
10-Jun-2014 |
Thomas Sewell <thomas.sewell@nicta.com.au> |
Hypsubst preserves equality hypotheses
Fixes included for various theories affected by this change.
--HG--
extra : rebase_source : b0150e06a14c2821e03208834282be6eca87aae0
|
| #
713cd402 |
|
13-Mar-2014 |
nipkow <none@none> |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
--HG--
extra : rebase_source : 4103bf02b2df95e1e84808f766f131292beef893
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
0c1e20b2 |
|
10-Jan-2012 |
berghofe <none@none> |
Replaced perm_set_eq by perm_set_def
|
| #
ed418196 |
|
28-Dec-2011 |
wenzelm <none@none> |
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
tuned proofs;
|
| #
4f35f893 |
|
13-Aug-2011 |
huffman <none@none> |
HOL-Nominal-Examples: respect distinction between sets and functions
|
| #
9027a081 |
|
03-Mar-2011 |
wenzelm <none@none> |
eliminated prems;
|
| #
4c4354d5 |
|
22-Apr-2010 |
wenzelm <none@none> |
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;
|