| Mon, 16 Sep 2013 12:27:20 +0200 |
review of examples for non-termination of rls norm_Rational
|
file | diff | annotate |
| Mon, 16 Sep 2013 12:20:00 +0200 |
Test_Isac works again, perfectly ..
|
file | diff | annotate |
| Mon, 16 Sep 2013 11:28:43 +0200 |
gcd_poly requires special handling for a monomial argument
|
file | diff | annotate |
| Mon, 02 Sep 2013 16:16:08 +0200 |
Test_Isac works again, almost ..
|
file | diff | annotate |
| Mon, 02 Sep 2013 15:17:34 +0200 |
GCD_Poly_ML: survey on levels integrating gcd_poly in Rational.thy
|
file | diff | annotate |
| Fri, 30 Aug 2013 13:43:30 +0200 |
GCD_Poly_ML: rewrite cancel is NONE if gcd_poly is 1
|
file | diff | annotate |
| Wed, 28 Aug 2013 11:48:37 +0200 |
GCD_Poly_ML: test 2nd level integration of gcd_poly
|
file | diff | annotate |
| Wed, 28 Aug 2013 11:02:03 +0200 |
GCD_Poly_ML: correct & improve assumptions generated from gcd_pol
|
file | diff | annotate |
| Wed, 28 Aug 2013 10:40:53 +0200 |
GCD_Poly_ML: test 1st level integration of gcd_poly
|
file | diff | annotate |
| Mon, 26 Aug 2013 16:32:21 +0200 |
tuned
|
file | diff | annotate |
| Sat, 24 Aug 2013 17:41:40 +0200 |
GCD_Poly_ML: integrated tests, reactivated test/../rational.sml
|
file | diff | annotate |
| Sat, 24 Aug 2013 11:54:39 +0200 |
GCD_Poly_ML: conversions term <--> poly
|
file | diff | annotate |
| Sat, 24 Aug 2013 11:18:43 +0200 |
GCD_Poly_ML: reformat specific part of rewriter
|
file | diff | annotate |
| Wed, 05 Dec 2012 10:21:35 +0100 |
collected non-termination in gcd_poly from Isabelle2002
|
file | diff | annotate |
| Sun, 14 Oct 2012 20:00:27 +0200 |
2011-->2012: ...
|
file | diff | annotate |
| Sun, 29 Jul 2012 16:29:04 +0200 |
prepare for stepToErrorPattern
|
file | diff | annotate |
| Wed, 13 Jun 2012 10:30:33 +0200 |
errpats for cancel
|
file | diff | annotate |
| Sat, 17 Mar 2012 12:52:30 +0100 |
uncomment test/../root,equation,poly.sml (Isabelle 2002 --> 2011)
|
file | diff | annotate |
| Thu, 06 Oct 2011 17:43:00 +0200 |
intermed. Build_Inverse_Z_Transform:
|
file | diff | annotate |
| Fri, 18 Mar 2011 09:26:03 +0100 |
intermed. usecase Diophant
|
file | diff | annotate |
| Thu, 17 Mar 2011 10:46:02 +0100 |
intermed usecase Diophant
|
file | diff | annotate |
| Thu, 17 Mar 2011 10:11:18 +0100 |
intermed. usecase Diophant
|
file | diff | annotate |
| Mon, 14 Mar 2011 16:50:44 +0100 |
intermed.update Isabelle2011: tests finished...
|
file | diff | annotate |
| Thu, 10 Mar 2011 17:05:09 +0100 |
intermed.update Isabelle2011: Not --> HOL.Not
|
file | diff | annotate |
| Thu, 10 Mar 2011 16:04:00 +0100 |
intermed.update Isabelle2011: HOL.True
|
file | diff | annotate |
| Fri, 31 Dec 2010 14:54:02 +0100 |
removed error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))
|
file | diff | annotate |
| Wed, 29 Dec 2010 20:07:52 +0100 |
intermed. in course/T3_MathEngine.thy
|
file | diff | annotate |
| Tue, 05 Oct 2010 16:46:56 +0200 |
repaired 'fun calc_equ' for "op <", completed rewriting in test/../rational.sml
|
file | diff | annotate |
| Tue, 05 Oct 2010 14:41:16 +0200 |
intermed. test/../rational.sml, before "op *" --> "Orderings.ord_class.less"
|
file | diff | annotate |
| Tue, 05 Oct 2010 09:17:48 +0200 |
updated print_exn
|
file | diff | annotate |
| Tue, 05 Oct 2010 08:35:55 +0200 |
intermed. test/../rational.sml
|
file | diff | annotate |
| Tue, 28 Sep 2010 10:10:26 +0200 |
updated "op *" --> Groups.times_class.times in src and test
|
file | diff | annotate |
| Tue, 28 Sep 2010 09:06:56 +0200 |
tuned error and writeln
|
file | diff | annotate |
| Wed, 08 Sep 2010 16:47:22 +0200 |
tuned src + test
|
file | diff | annotate |
| Mon, 06 Sep 2010 14:48:38 +0200 |
updated Knowledge/PolyMinus, plus some changes ahead
|
file | diff | annotate |
| Fri, 03 Sep 2010 17:19:20 +0200 |
updated Knowledge/Rational
|
file | diff | annotate |
| Wed, 01 Sep 2010 15:17:43 +0200 |
fixed all @{thm } in src+test
|
file | diff | annotate |
| Tue, 31 Aug 2010 16:38:22 +0200 |
updating Knowledge/Simplify, changes ahead + in test
|
file | diff | annotate |
| Mon, 30 Aug 2010 14:35:51 +0200 |
renamed test/* according to src/*
|
file | diff | annotate | base |