src/HOL/Decision_Procs/Polynomial_List.thy
changeset 33268 02de0317f66f
parent 33153 92080294beb8
child 35028 108662d50512
     1.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Oct 28 00:23:39 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Wed Oct 28 00:24:38 2009 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4 -(*  Title:       HOL/Decision_Procs/Polynomial_List.thy
     1.5 -    Author:      Amine Chaieb
     1.6 +(*  Title:      HOL/Decision_Procs/Polynomial_List.thy
     1.7 +    Author:     Amine Chaieb
     1.8  *)
     1.9  
    1.10 -header{*Univariate Polynomials as Lists *}
    1.11 +header {* Univariate Polynomials as Lists *}
    1.12  
    1.13  theory Polynomial_List
    1.14  imports Main
    1.15 @@ -653,7 +653,7 @@
    1.16  apply (simp add: divides_def fun_eq poly_mult)
    1.17  apply (rule_tac x = "[]" in exI)
    1.18  apply (auto dest!: order2 [where a=a]
    1.19 -	    intro: poly_exp_divides simp del: pexp_Suc)
    1.20 +            intro: poly_exp_divides simp del: pexp_Suc)
    1.21  done
    1.22  
    1.23  lemma order_decomp:
    1.24 @@ -780,4 +780,5 @@
    1.25  done
    1.26  
    1.27  lemma poly_Sing: "poly [c] x = c" by simp
    1.28 +
    1.29  end