Walther Neuper <neuper@ist.tugraz.at> [Fri, 31 May 2013 17:50:33 +0200] rev 48872
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 31 May 2013 17:49:34 +0200] rev 48871
GCD_Poly.thy with writeln for try_new_prime_up
writeln used for testing codegen
Walther Neuper <neuper@ist.tugraz.at> [Fri, 24 May 2013 16:50:31 +0200] rev 48870
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 24 May 2013 14:25:34 +0200] rev 48869
GCD_Poly.thy restored (without writeln)
Walther Neuper <neuper@ist.tugraz.at> [Fri, 24 May 2013 12:40:15 +0200] rev 48868
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 24 May 2013 10:41:57 +0200] rev 48867
GCD_Poly.thy with writeln for HENSEL
Walther Neuper <neuper@ist.tugraz.at> [Thu, 23 May 2013 12:29:02 +0200] rev 48866
tuned
Walther Neuper <neuper@ist.tugraz.at> [Thu, 23 May 2013 12:20:28 +0200] rev 48865
GCD_Poly_FP.thy all termination proofs checked with size_change
size_change seems not appropriate for CA.
The key for progress is make_primes => next_prime_not_dvd => HENSEL_lifting_up.
The most difficult termination proof seems try_new_prime_up.
Walther Neuper <neuper@ist.tugraz.at> [Tue, 21 May 2013 11:33:03 +0200] rev 48864
GCD_Poly_FP.thy formatted according to 2013/../List.thy
Walther Neuper <neuper@ist.tugraz.at> [Tue, 21 May 2013 10:38:16 +0200] rev 48863
GCD_Poly_FP.thy all termination proofs checked
checked for simple provability, imperfect state documented here.
+ improved some int / nat signature(s)
+ replaced "nth" by "!"