| Wed, 28 Aug 2013 11:48:37 +0200 |
Walther Neuper |
GCD_Poly_ML: test 2nd level integration of gcd_poly
|
changeset |
files
|
| Wed, 28 Aug 2013 11:02:03 +0200 |
Walther Neuper |
GCD_Poly_ML: correct & improve assumptions generated from gcd_pol
|
changeset |
files
|
| Wed, 28 Aug 2013 10:40:53 +0200 |
Walther Neuper |
GCD_Poly_ML: test 1st level integration of gcd_poly
|
changeset |
files
|
| Mon, 26 Aug 2013 16:32:21 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 26 Aug 2013 15:37:48 +0200 |
Walther Neuper |
GCD_Poly_ML: integrated gcd_poly into Rational.thy
|
changeset |
files
|
| Mon, 26 Aug 2013 11:20:41 +0200 |
Walther Neuper |
Test_Isac doesn't work anymore
|
changeset |
files
|
| Mon, 26 Aug 2013 10:52:54 +0200 |
Walther Neuper |
GCD_Poly_ML: deleted unused code for cancellation and add.of.fract
|
changeset |
files
|
| Sat, 24 Aug 2013 17:41:40 +0200 |
Walther Neuper |
GCD_Poly_ML: integrated tests, reactivated test/../rational.sml
|
changeset |
files
|
| Sat, 24 Aug 2013 11:54:39 +0200 |
Walther Neuper |
GCD_Poly_ML: conversions term <--> poly
|
changeset |
files
|
| Sat, 24 Aug 2013 11:23:34 +0200 |
Walther Neuper |
GCD_Poly_ML: minimise negative coefficients
|
changeset |
files
|
| Sat, 24 Aug 2013 11:18:43 +0200 |
Walther Neuper |
GCD_Poly_ML: reformat specific part of rewriter
|
changeset |
files
|
| Fri, 23 Aug 2013 09:32:05 +0200 |
Walther Neuper |
GCD_Poly_ML: start integration into Isac by commenting datatypes
|
changeset |
files
|
| Sat, 17 Aug 2013 15:45:36 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sat, 17 Aug 2013 15:43:24 +0200 |
Walther Neuper |
unsuccessful investigation of failing evaluation
|
changeset |
files
|
| Wed, 14 Aug 2013 17:14:11 +0200 |
Walther Neuper |
large numerals: which evaluation strategy is used ?
|
changeset |
files
|
| Wed, 14 Aug 2013 16:30:47 +0200 |
Walther Neuper |
GCD_Poly: Euclidean algorithm evaluates efficiently with large numerals
|
changeset |
files
|
| Wed, 14 Aug 2013 14:32:18 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Wed, 14 Aug 2013 14:05:40 +0200 |
Walther Neuper |
suggestions for representation of calculations and interaction by Lucas-Interpretation
|
changeset |
files
|
| Wed, 14 Aug 2013 13:52:39 +0200 |
Walther Neuper |
GCD_Poly: removed bug in polynomial division
|
changeset |
files
|
| Wed, 14 Aug 2013 13:21:24 +0200 |
Walther Neuper |
code generated from GCD_Poly.thy
|
changeset |
files
|
| Wed, 14 Aug 2013 13:15:42 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Thu, 25 Jul 2013 07:53:39 +0200 |
Walther Neuper |
handle "fun nth " from Isabelle2002 still provisionally
|
changeset |
files
|
| Thu, 25 Jul 2013 07:36:31 +0200 |
Walther Neuper |
restructured files concerning "fun gcd_poly"
|
changeset |
files
|
| Wed, 24 Jul 2013 16:06:06 +0200 |
Walther Neuper |
Euclidean Algorithm naively used on polynomials
|
changeset |
files
|
| Mon, 22 Jul 2013 14:09:26 +0200 |
Walther Neuper |
started trials with Library/Polynomial.thy
|
changeset |
files
|
| Mon, 22 Jul 2013 13:52:18 +0200 |
Walther Neuper |
--- Test_Isac.thy runs all tests
|
changeset |
files
|
| Sun, 21 Jul 2013 15:15:50 +0200 |
Walther Neuper |
removed ERROR: Undefined session(s): "Isac"
|
changeset |
files
|
| Sun, 21 Jul 2013 15:11:01 +0200 |
Walther Neuper |
merged
|
changeset |
files
|
| Thu, 18 Jul 2013 14:31:58 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Thu, 18 Jul 2013 14:30:58 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sun, 21 Jul 2013 15:08:31 +0200 |
Walther Neuper |
a bulky chunk of changes
|
changeset |
files
|
| Sat, 20 Jul 2013 08:07:39 +0200 |
Walther Neuper |
hint for transition to Isabelle's numerals, cf. num_str
|
changeset |
files
|
| Thu, 18 Jul 2013 14:26:49 +0200 |
Walther Neuper |
GCD_Poly trials with naive Euclidean Algorithm
|
changeset |
files
|
| Wed, 17 Jul 2013 07:32:53 +0200 |
Walther Neuper |
--- heap image for Isac on Isabelle2013 builds
|
changeset |
files
|
| Mon, 15 Jul 2013 08:28:50 +0200 |
Walther Neuper |
--- Build_Isac.thy runs on Isabelle2013
|
changeset |
files
|
| Mon, 15 Jul 2013 07:50:28 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 15 Jul 2013 06:12:51 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Mon, 15 Jul 2013 06:05:32 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sun, 14 Jul 2013 15:02:09 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sun, 14 Jul 2013 14:48:14 +0200 |
Walther Neuper |
merged
|
changeset |
files
|
| Sun, 14 Jul 2013 14:24:41 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
| Sun, 14 Jul 2013 09:04:18 +0200 |
Walther Neuper |
--- Isabelle's hgignore replaced by isac's hgignore
|
changeset |
files
|
| Mon, 11 Feb 2013 14:39:04 +0100 |
wenzelm |
make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;
|
changeset |
files
|
| Sun, 10 Feb 2013 22:07:56 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Sun, 10 Feb 2013 22:03:21 +0100 |
wenzelm |
avoid crash (NPE) when properties are changed during prover startup (e.g. by font scaling);
|
changeset |
files
|
| Sun, 10 Feb 2013 14:57:00 +0100 |
wenzelm |
updated PIDE notes;
|
changeset |
files
|
| Thu, 07 Feb 2013 13:20:05 +0100 |
wenzelm |
proper root for document variants (cf. be8002ee43d8);
|
changeset |
files
|
| Thu, 07 Feb 2013 12:08:37 +0100 |
wenzelm |
Added tag Isabelle2013-RC3 for changeset 8cf38c6b33f8
|
changeset |
files
|
| Wed, 06 Feb 2013 23:14:50 +0100 |
wenzelm |
proforma update to jdk-7u13 -- barely relevant security updates by Oracle;
|
changeset |
files
|
| Wed, 06 Feb 2013 21:05:06 +0100 |
wenzelm |
more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
|
changeset |
files
|
| Wed, 06 Feb 2013 20:03:42 +0100 |
wenzelm |
documentation for 'print_rules';
|
changeset |
files
|
| Fri, 01 Feb 2013 22:24:27 +0100 |
wenzelm |
no choice of target directory -- default file permissions outside user directory tend to be ill-defined for Cygwin;
|
changeset |
files
|
| Fri, 01 Feb 2013 21:58:13 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 01 Feb 2013 21:58:00 +0100 |
wenzelm |
provide jdk-7u13 (still inactive, potentially pointless);
|
changeset |
files
|
| Fri, 01 Feb 2013 21:40:15 +0100 |
wenzelm |
allow relative directory;
|
changeset |
files
|
| Fri, 01 Feb 2013 21:31:21 +0100 |
wenzelm |
standardized isabelle-server.in.tum.de;
|
changeset |
files
|
| Thu, 31 Jan 2013 22:21:05 +0100 |
wenzelm |
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
|
changeset |
files
|
| Mon, 28 Jan 2013 23:56:13 +0100 |
traytel |
made SML/NJ happy
|
changeset |
files
|
| Mon, 28 Jan 2013 22:37:58 +0100 |
wenzelm |
more portable alternative shortcuts on numeric keypad;
|
changeset |
files
|
| Mon, 28 Jan 2013 17:37:09 +0100 |
wenzelm |
more generic reference to polyml component;
|
changeset |
files
|