| Fri, 24 Aug 2018 14:23:13 +0200 |
Isabelle2017->18: for Test_Isac.thy adopt new comments
|
file | diff | annotate |
| Fri, 09 Feb 2018 12:12:25 +0100 |
Isabelle2015->17: imports of Text_Isac work again
|
file | diff | annotate |
| Wed, 07 Feb 2018 11:27:38 +0100 |
Isabelle2015->17: session identifiers enforced now
|
file | diff | annotate |
| Wed, 07 Feb 2018 11:21:54 +0100 |
Isabelle2015->17: header in thys dropped
|
file | diff | annotate |
| Tue, 06 Feb 2018 16:54:05 +0100 |
Isabelle2015->17: Polynomial.thy etc has been shifted
|
file | diff | annotate |
| Mon, 21 Dec 2015 14:19:03 +0100 |
Isabelle2014-->15: Test_Isac is perfect
|
file | diff | annotate |
| Mon, 21 Dec 2015 13:58:02 +0100 |
Isabelle2014-->2015: dropped tests not required any more
|
file | diff | annotate |
| Wed, 13 Nov 2013 15:10:21 +0100 |
restored tests on Polynomials, cf 11557b906ac1
|
file | diff | annotate |
| Tue, 12 Nov 2013 17:40:11 +0100 |
keep comments in HOL theories
|
file | diff | annotate |
| Fri, 27 Sep 2013 17:42:16 +0200 |
Test_Isac needs check for errors in the imported theories in the <Theories> window
|
file | diff | annotate |
| Sun, 21 Jul 2013 15:08:31 +0200 |
a bulky chunk of changes
|
file | diff | annotate |
| Tue, 11 Jun 2013 09:06:29 +0200 |
GCD_Poly_FP.thy termination clarified with Florian Haftmann
|
file | diff | annotate |
| Sun, 09 Jun 2013 09:26:10 +0200 |
exact state after Florian left
|
file | diff | annotate |
| Thu, 06 Jun 2013 20:39:40 +0200 |
Florian Haftmann intermediate
|
file | diff | annotate |
| Mon, 03 Jun 2013 16:20:11 +0200 |
investigating: export_code for try_new_prime_up
|
file | diff | annotate |
| Fri, 31 May 2013 17:49:34 +0200 |
GCD_Poly.thy with writeln for try_new_prime_up
|
file | diff | annotate |
| Fri, 24 May 2013 16:50:31 +0200 |
tuned
|
file | diff | annotate |
| Thu, 23 May 2013 12:20:28 +0200 |
GCD_Poly_FP.thy all termination proofs checked with size_change
|
file | diff | annotate |
| Tue, 21 May 2013 11:33:03 +0200 |
GCD_Poly_FP.thy formatted according to 2013/../List.thy
|
file | diff | annotate |
| Tue, 21 May 2013 10:38:16 +0200 |
GCD_Poly_FP.thy all termination proofs checked
|
file | diff | annotate |
| Sun, 19 May 2013 08:51:27 +0200 |
GCD_Poly_FP.thy improved with nat as much as possible instead int
|
file | diff | annotate |
| Mon, 13 May 2013 12:08:14 +0200 |
intermed. GCD_Poly_FP.thy termination
|
file | diff | annotate |
| Fri, 10 May 2013 10:47:23 +0200 |
GCD_Poly_FP.thy finished for univariate case
|
file | diff | annotate |
| Fri, 10 May 2013 10:22:39 +0200 |
gcd_up works again
|
file | diff | annotate |
| Thu, 09 May 2013 17:04:01 +0200 |
before backtracing to working gcd_up
|
file | diff | annotate |
| Tue, 07 May 2013 12:22:07 +0200 |
polish GCD_Poly.thy
|
file | diff | annotate |
| Mon, 06 May 2013 19:14:35 +0200 |
tuned
|
file | diff | annotate |
| Mon, 06 May 2013 18:21:10 +0200 |
GCD_Poly_FP.thy code for univariate case finished
|
file | diff | annotate |
| Thu, 25 Apr 2013 18:49:52 +0200 |
polish GCD_Poly.thy: until gcd_poly'
|
file | diff | annotate |
| Thu, 25 Apr 2013 13:58:36 +0200 |
polish GCD_Poly.thy: lex_ord interm.
|
file | diff | annotate |
| Sat, 20 Apr 2013 15:01:16 +0200 |
polish GCD_Poly.thy: lcoeff
|
file | diff | annotate |
| Fri, 12 Apr 2013 20:46:58 +0200 |
polished GCD_Poly.thy
|
file | diff | annotate |
| Fri, 12 Apr 2013 11:03:41 +0200 |
before finalizing GCD_Poly.thy
|
file | diff | annotate |
| Thu, 21 Mar 2013 15:40:13 +0100 |
GCD_Poly ML-->Isabelle: simplified dvd for univariate polynomials
|
file | diff | annotate |
| Mon, 18 Mar 2013 10:46:37 +0100 |
GCD_Poly ML-->Isabelle: intermediate
|
file | diff | annotate |
| Wed, 06 Mar 2013 09:37:17 +0100 |
GCD_Poly ML-->Isabelle: intermediate
|
file | diff | annotate |
| Thu, 28 Feb 2013 16:28:28 +0100 |
GCD_Poly ML-->Isabelle: fun %|% (function dvd_up)
|
file | diff | annotate |
| Mon, 25 Feb 2013 13:27:38 +0100 |
primes_upto: removed tracing
|
file | diff | annotate |
| Mon, 25 Feb 2013 11:46:04 +0100 |
primes_upto re-uses primes already calculated
|
file | diff | annotate |
| Sat, 23 Feb 2013 10:14:50 +0100 |
GCD_Poly ML-->Isabelle: intermediate
|
file | diff | annotate |
| Fri, 22 Feb 2013 12:07:27 +0100 |
GCD_Poly ML-->Isabelle: implicit specifications
|
file | diff | annotate |
| Tue, 19 Feb 2013 13:56:35 +0100 |
GCD_Poly ML-->Isabelle: intermed.
|
file | diff | annotate |
| Fri, 15 Feb 2013 15:46:29 +0100 |
tuned
|
file | diff | annotate |
| Fri, 15 Feb 2013 14:49:50 +0100 |
GCD_Poly ML-->Isabelle: waiting for feedback from isabelle@
|
file | diff | annotate |
| Tue, 12 Feb 2013 09:22:20 +0100 |
intermed.
|
file | diff | annotate |
| Fri, 08 Feb 2013 16:43:04 +0100 |
GCD_Poly ML-->Isabelle: until fun mod_poly_gcd
|
file | diff | annotate |
| Mon, 04 Feb 2013 12:41:56 +0100 |
intermed.
|
file | diff | annotate |
| Tue, 29 Jan 2013 13:42:00 +0100 |
GCD_Poly ML-->Isabelle: intermediate
|
file | diff | annotate |
| Mon, 28 Jan 2013 13:53:07 +0100 |
GCD_Poly ML-->Isabelle: until fun dvd_up
|
file | diff | annotate |
| Thu, 24 Jan 2013 17:17:03 +0100 |
GCD_Poly ML-->Isabelle: until fun %-%
|
file | diff | annotate |
| Wed, 23 Jan 2013 17:29:49 +0100 |
GCD_Poly ML-->Isabelle: ordered tests
|
file | diff | annotate |
| Wed, 23 Jan 2013 15:56:24 +0100 |
GCD_Poly: ML --> Isabelle's function package
|
file | diff | annotate |