src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 42814 5af15f1e2ef6
parent 42368 3b8498ac2314
child 44013 5cfc1c36ae97
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun May 15 17:06:35 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun May 15 17:45:53 2011 +0200
     1.3 @@ -3044,7 +3044,7 @@
     1.4   (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
     1.5    (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar_tac T ps ctxt))
     1.6  end
     1.7 -*} "Parametric QE for linear Arithmetic over fields, Version 1"
     1.8 +*} "parametric QE for linear Arithmetic over fields, Version 1"
     1.9  
    1.10  method_setup frpar2 = {*
    1.11  let
    1.12 @@ -3061,7 +3061,7 @@
    1.13   (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
    1.14    (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar2_tac T ps ctxt))
    1.15  end
    1.16 -*} "Parametric QE for linear Arithmetic over fields, Version 2"
    1.17 +*} "parametric QE for linear Arithmetic over fields, Version 2"
    1.18  
    1.19  
    1.20  lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"