| Sun, 03 Nov 2019 19:59:56 -0500 |
immler |
refactor Approximation.thy to use more abstract type of intervals
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 21:46:46 -0500 |
immler |
replace approximation oracle by less ad-hoc @{computation}s
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 21 Nov 2016 15:30:35 +0100 |
immler |
op powr for quickcheck[approximation] (amending 67792e4a5486)
|
file |
diff |
annotate
|
| Wed, 21 Sep 2016 17:56:25 +0200 |
immler |
approximation: preprocessing for nat/int expressions
|
file |
diff |
annotate
|
| Wed, 21 Sep 2016 17:56:25 +0200 |
immler |
approximation: rewrite for reduction to base expressions
|
file |
diff |
annotate
|
| Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 10:52:54 +0200 |
eberlm |
exposed approximation in ML
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:33:25 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 17:37:43 +0100 |
immler |
added quickcheck[approximation]
|
file |
diff |
annotate
|