src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 41413 64cd30d6b0b8
parent 39246 9e58f0499f57
child 41807 ab5d2d81f9fb
child 41809 6799f95479e2
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Dec 29 13:51:17 2010 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Dec 29 17:34:41 2010 +0100
     1.3 @@ -5,9 +5,10 @@
     1.4  header{* A formalization of Ferrante and Rackoff's procedure with polynomial parameters, see Paper in CALCULEMUS 2008 *}
     1.5  
     1.6  theory Parametric_Ferrante_Rackoff
     1.7 -imports Reflected_Multivariate_Polynomial
     1.8 +imports
     1.9 +  Reflected_Multivariate_Polynomial
    1.10    Dense_Linear_Order
    1.11 -  Efficient_Nat
    1.12 +  "~~/src/HOL/Library/Efficient_Nat"
    1.13  begin
    1.14  
    1.15  subsection {* Terms *}