Tue, 22 May 2012 19:02:17 +0200 |
wenzelm |
Added tag Isabelle2012 for changeset 21c42b095c84
|
changeset |
files
|
Sun, 14 Jul 2013 14:13:44 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Sun, 14 Jul 2013 09:58:28 +0200 |
Walther Neuper |
--- prepared isac for being fetched into Isabelle2013's repository
|
changeset |
files
|
Fri, 12 Jul 2013 06:39:55 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Thu, 11 Jul 2013 16:59:05 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Thu, 11 Jul 2013 16:58:31 +0200 |
Walther Neuper |
end of improving tests for isac on Isabelle2012
|
changeset |
files
|
Sun, 30 Jun 2013 17:27:34 +0200 |
Walther Neuper |
Test_Isac.thy without errors on Isabelle2012, calchead.sml:
|
changeset |
files
|
Fri, 21 Jun 2013 17:53:46 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Fri, 21 Jun 2013 17:49:24 +0200 |
Walther Neuper |
Test_Isac.thy without errors on Isabelle2012, rewtools.sml:
|
changeset |
files
|
Fri, 21 Jun 2013 11:19:18 +0200 |
Walther Neuper |
Test_Isac.thy without errors on Isabelle2012, intermediate
|
changeset |
files
|
Fri, 21 Jun 2013 08:06:50 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Fri, 21 Jun 2013 08:06:16 +0200 |
Walther Neuper |
plans for isac's transitions Isabelle2011-->12 in more detail; errors in tests
|
changeset |
files
|
Fri, 21 Jun 2013 06:51:11 +0200 |
Walther Neuper |
irrelevant cleaning
|
changeset |
files
|
Thu, 20 Jun 2013 17:53:47 +0200 |
Walther Neuper |
manually completed "thehier" such that insert_errpats, insert_fillpats
|
changeset |
files
|
Thu, 20 Jun 2013 11:26:56 +0200 |
Walther Neuper |
plans for isac's transitions Isabelle2011-->12 and Isabelle2012-->13
|
changeset |
files
|
Tue, 18 Jun 2013 17:56:09 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Tue, 18 Jun 2013 17:51:36 +0200 |
Walther Neuper |
Test_Isac.thy started in Isabelle2012
|
changeset |
files
|
Tue, 18 Jun 2013 08:19:57 +0200 |
Walther Neuper |
Build_Isac.thy and creating Isac heap OK
|
changeset |
files
|
Sun, 16 Jun 2013 13:18:10 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Sun, 16 Jun 2013 13:10:32 +0200 |
Walther Neuper |
Isabelle2011 --> 2012 intermediate: find appropriate Isac binary
|
changeset |
files
|
Sun, 16 Jun 2013 12:31:41 +0200 |
Walther Neuper |
Isabelle2011 --> 2012 intermediate
|
changeset |
files
|
Fri, 14 Jun 2013 15:46:09 +0200 |
Walther Neuper |
interrupt GCD_Poly.ML making transparent, resume Isabelle2011 -> 2012
|
changeset |
files
|
Tue, 11 Jun 2013 09:06:29 +0200 |
Walther Neuper |
GCD_Poly_FP.thy termination clarified with Florian Haftmann
|
changeset |
files
|
Sun, 09 Jun 2013 09:26:10 +0200 |
Walther Neuper |
exact state after Florian left
|
changeset |
files
|
Thu, 06 Jun 2013 20:39:40 +0200 |
Walther Neuper |
Florian Haftmann intermediate
|
changeset |
files
|
Mon, 03 Jun 2013 16:20:11 +0200 |
Walther Neuper |
investigating: export_code for try_new_prime_up
|
changeset |
files
|
Fri, 31 May 2013 18:05:20 +0200 |
Walther Neuper |
GCD_Poly.thy restored (without writeln)
|
changeset |
files
|
Fri, 31 May 2013 18:00:35 +0200 |
Walther Neuper |
export_code for try_new_prime_up and gcd_up
|
changeset |
files
|
Fri, 31 May 2013 17:50:33 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Fri, 31 May 2013 17:49:34 +0200 |
Walther Neuper |
GCD_Poly.thy with writeln for try_new_prime_up
|
changeset |
files
|
Fri, 24 May 2013 16:50:31 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Fri, 24 May 2013 14:25:34 +0200 |
Walther Neuper |
GCD_Poly.thy restored (without writeln)
|
changeset |
files
|
Fri, 24 May 2013 12:40:15 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Fri, 24 May 2013 10:41:57 +0200 |
Walther Neuper |
GCD_Poly.thy with writeln for HENSEL
|
changeset |
files
|
Thu, 23 May 2013 12:29:02 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Thu, 23 May 2013 12:20:28 +0200 |
Walther Neuper |
GCD_Poly_FP.thy all termination proofs checked with size_change
|
changeset |
files
|
Tue, 21 May 2013 11:33:03 +0200 |
Walther Neuper |
GCD_Poly_FP.thy formatted according to 2013/../List.thy
|
changeset |
files
|
Tue, 21 May 2013 10:38:16 +0200 |
Walther Neuper |
GCD_Poly_FP.thy all termination proofs checked
|
changeset |
files
|
Sun, 19 May 2013 08:51:27 +0200 |
Walther Neuper |
GCD_Poly_FP.thy improved with nat as much as possible instead int
|
changeset |
files
|
Mon, 13 May 2013 12:08:14 +0200 |
Walther Neuper |
intermed. GCD_Poly_FP.thy termination
|
changeset |
files
|
Fri, 10 May 2013 10:47:23 +0200 |
Walther Neuper |
GCD_Poly_FP.thy finished for univariate case
|
changeset |
files
|
Fri, 10 May 2013 10:22:39 +0200 |
Walther Neuper |
gcd_up works again
|
changeset |
files
|
Thu, 09 May 2013 17:04:01 +0200 |
Walther Neuper |
before backtracing to working gcd_up
|
changeset |
files
|
Tue, 07 May 2013 12:22:07 +0200 |
Walther Neuper |
polish GCD_Poly.thy
|
changeset |
files
|
Mon, 06 May 2013 19:14:35 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Mon, 06 May 2013 18:21:10 +0200 |
Walther Neuper |
GCD_Poly_FP.thy code for univariate case finished
|
changeset |
files
|
Wed, 01 May 2013 11:59:33 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Wed, 01 May 2013 11:52:37 +0200 |
Walther Neuper |
GCD_Poly.thy tuned
|
changeset |
files
|
Sat, 27 Apr 2013 12:27:38 +0200 |
Walther Neuper |
tuned
|
changeset |
files
|
Sat, 27 Apr 2013 12:23:46 +0200 |
Walther Neuper |
GCD_Poly.thy as submitted to Munich
|
changeset |
files
|
Thu, 25 Apr 2013 18:49:52 +0200 |
Walther Neuper |
polish GCD_Poly.thy: until gcd_poly'
|
changeset |
files
|
Thu, 25 Apr 2013 13:58:36 +0200 |
Walther Neuper |
polish GCD_Poly.thy: lex_ord interm.
|
changeset |
files
|
Sat, 20 Apr 2013 18:18:06 +0200 |
Walther Neuper |
polish GCD_Poly.thy: lmonom done
|
changeset |
files
|
Sat, 20 Apr 2013 15:01:16 +0200 |
Walther Neuper |
polish GCD_Poly.thy: lcoeff
|
changeset |
files
|
Fri, 12 Apr 2013 20:46:58 +0200 |
Walther Neuper |
polished GCD_Poly.thy
|
changeset |
files
|
Fri, 12 Apr 2013 11:03:41 +0200 |
Walther Neuper |
before finalizing GCD_Poly.thy
|
changeset |
files
|
Thu, 21 Mar 2013 15:40:13 +0100 |
Walther Neuper |
GCD_Poly ML-->Isabelle: simplified dvd for univariate polynomials
|
changeset |
files
|
Mon, 18 Mar 2013 10:46:55 +0100 |
Walther Neuper |
merged
|
changeset |
files
|
Mon, 18 Mar 2013 10:46:37 +0100 |
Walther Neuper |
GCD_Poly ML-->Isabelle: intermediate
|
changeset |
files
|
Sat, 16 Mar 2013 14:52:02 +0100 |
diana |
GCD_POLY -> new fun %%/%%
|
changeset |
files
|