| Tue, 22 May 2018 11:08:37 +0200 |
nipkow |
First step to remove nonstandard "[x <- xs. P]" syntax: only input
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 21:51:44 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 11:24:34 +0200 |
wenzelm |
eliminated \<Colon> -- from dead code!
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 17:07:44 +0200 |
Andreas Lochbihler |
reactivate examples with predicate compiler and quickcheck
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
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
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adapting predicate_compile_quickcheck
|
file |
diff |
annotate
|
| Thu, 23 Sep 2010 14:50:14 +0200 |
bulwahn |
handling equivalences smarter in the predicate compiler
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 11:51:53 +0200 |
bulwahn |
using linear find_least instead of sorting in the mode analysis of the predicate compiler
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 17:30:56 +0200 |
bulwahn |
adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 17:40:44 +0100 |
bulwahn |
added predicate compiler quickcheck examples to new session Predicate_Compile_Examples
|
file |
diff |
annotate
|