| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Fri, 30 Dec 2016 15:40:35 +0100 |
blanchet |
more uniform errors in '(prim)(co)rec(ursive)' variants
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 17:22:16 +0100 |
blanchet |
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
|
file |
diff |
annotate
|
| Thu, 22 Dec 2016 19:14:58 +0100 |
blanchet |
export ML functions (towards nonuniform codatatypes) + signature tuning
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 12:49:15 +0100 |
blanchet |
generalized ML function (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Wed, 14 Dec 2016 09:19:50 +0100 |
blanchet |
only recognize maps if the type names match
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 20:32:02 +0200 |
blanchet |
robustness
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 11:55:39 +0200 |
blanchet |
extended ML signature + refactored
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 17:52:08 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:41:11 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Tue, 31 May 2016 11:54:45 +0200 |
blanchet |
made parsing of monomorphic/polymorphic constants more robust
|
file |
diff |
annotate
|
| Tue, 31 May 2016 10:53:11 +0200 |
blanchet |
more flexible parsing (towards type class support)
|
file |
diff |
annotate
|
| Mon, 30 May 2016 14:15:44 +0200 |
wenzelm |
allow 'for' fixes for multi_specs;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 20:54:17 +0200 |
wenzelm |
prefer binding over base name;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 14:38:57 +0200 |
wenzelm |
Type_Infer.object_logic controls improvement of type inference result;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 19:17:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 18:07:55 +0200 |
blanchet |
more natural order for 'cong_intros'
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 10:57:02 +0200 |
blanchet |
renamed generated theorem
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
avoid 'prove_sorry' for unreliable tactics
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
reused code
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
more reliable check for rhs variables
|
file |
diff |
annotate
|
| Wed, 23 Mar 2016 16:37:13 +0100 |
blanchet |
sorted out type issue with sort constraints
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 12:39:37 +0100 |
blanchet |
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
|
file |
diff |
annotate
|