Tue, 17 Sep 2013 10:12:15 +0200 |
Walther Neuper |
determined main-file for mlehnfeld's master thesis
|
changeset |
files
|
Tue, 17 Sep 2013 09:50:52 +0200 |
Walther Neuper |
separated Isac documentation (~~/doc-isac) from Isabelle documentation (~~/src/Doc)
|
changeset |
files
|
Mon, 16 Sep 2013 12:27:20 +0200 |
Walther Neuper |
review of examples for non-termination of rls norm_Rational
|
changeset |
files
|
Mon, 16 Sep 2013 12:20:00 +0200 |
Walther Neuper |
Test_Isac works again, perfectly ..
|
changeset |
files
|
Mon, 16 Sep 2013 11:28:43 +0200 |
Walther Neuper |
gcd_poly requires special handling for a monomial argument
|
changeset |
files
|
Mon, 16 Sep 2013 10:46:51 +0200 |
Walther Neuper |
tolerate Var in rewriting
|
changeset |
files
|
Fri, 13 Sep 2013 18:57:11 +0200 |
Walther Neuper |
Test_Theory without session Isac has limitations
|
changeset |
files
|
Mon, 02 Sep 2013 16:16:08 +0200 |
Walther Neuper |
Test_Isac works again, almost ..
|
changeset |
files
|
Mon, 02 Sep 2013 15:17:34 +0200 |
Walther Neuper |
GCD_Poly_ML: survey on levels integrating gcd_poly in Rational.thy
|
changeset |
files
|
Mon, 02 Sep 2013 14:56:57 +0200 |
Walther Neuper |
GCD_Poly_ML: generalised gcd_poly handling monomials
|
changeset |
files
|
Sun, 01 Sep 2013 16:50:51 +0200 |
Walther Neuper |
GCD_Poly_ML: removed bug in gcd_poly when applied to two monomials
|
changeset |
files
|
Sun, 01 Sep 2013 15:54:48 +0200 |
Walther Neuper |
GCD_Poly_ML: bug in gcd_poly when applied to two monomials
|
changeset |
files
|
Fri, 30 Aug 2013 13:43:30 +0200 |
Walther Neuper |
GCD_Poly_ML: rewrite cancel is NONE if gcd_poly is 1
|
changeset |
files
|
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
|