| #
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;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
1c79f041 |
|
13-Sep-2015 |
wenzelm <none@none> |
renamed method "goals" to "goal_cases" to emphasize its meaning;
|
| #
883895af |
|
31-Aug-2015 |
wenzelm <none@none> |
prefer symbols;
|
| #
5b7d639c |
|
25-Jun-2015 |
wenzelm <none@none> |
tuned proofs;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
9d496d0e |
|
12-Oct-2011 |
wenzelm <none@none> |
tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
|
| #
03b44894 |
|
03-Sep-2011 |
haftmann <none@none> |
tuned proof
|
| #
7a4b6a89 |
|
21-Feb-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
4d0c51ec |
|
30-Jan-2010 |
berghofe <none@none> |
Adapted to changes in cases method.
|
| #
f94fe110 |
|
10-Jan-2010 |
berghofe <none@none> |
Adapted to changes in induct method.
|
| #
b5d51d16 |
|
27-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
| #
7ebd3d61 |
|
26-Oct-2009 |
berghofe <none@none> |
Added Pattern.thy to Nominal/Examples.
|