| 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
|