1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_OLD.thy	Fri Aug 06 12:09:06 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_OLD.thy	Fri Aug 06 18:27:05 2021 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4          (*"~~/src/HOL/Number_Theory/Primes" ??? rm ???, thys for code_gen missing*)
     1.5        (*"~~/src/HOL/Library/Code_Target_Numeral"  ...note (4)*)
     1.6  begin
     1.7 +ML_file \<open>gcd_poly_old.sml\<close> (* this ML code was derived into the Isar code below *)
     1.8 +
     1.9  value "xxx" \<comment> \<open>TODO\<close>
    1.10  
    1.11  subsection \<open>Euclidean Algorithm with generalised division\<close>
    1.12 @@ -31,7 +33,7 @@
    1.13  Term:  \<lambda>a p n. coeff p n div a
    1.14  Type:  ?'b \<Rightarrow> ?'b poly \<Rightarrow> nat \<Rightarrow> ?'b
    1.15  
    1.16 -Reason:  The type of the term cannot be instancied to "'a \<Rightarrow> 'a poly \<Rightarrow> nat \<Rightarrow> 'a".
    1.17 +Reason:  The type of the term cannot be instantiated to "'a \<Rightarrow> 'a poly \<Rightarrow> nat \<Rightarrow> 'a".
    1.18  *)
    1.19  (*/------------------------------------------------------------------------------\
    1.20    this is an odd bypass for the above problem: