src/HOL/Library/positivstellensatz.ML
changeset 44058 ae85c5d64913
parent 39920 7479334d2c90
child 44454 6f28f96a09bf
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Aug 08 16:38:59 2011 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Aug 08 17:23:15 2011 +0200
     1.3 @@ -170,8 +170,8 @@
     1.4      Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) 
     1.5       (Thm.implies_intr (cprop_of tha) thb);
     1.6  
     1.7 -fun prove_hyp tha thb = 
     1.8 -  if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
     1.9 +fun prove_hyp tha thb =
    1.10 +  if exists (curry op aconv (concl_of tha)) (Thm.hyps_of thb)  (* FIXME !? *)
    1.11    then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
    1.12  
    1.13  val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and