src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
changeset 43946 ba88bb44c192
parent 42361 23f352990944
child 55508 90c42b130652
equal deleted inserted replaced
43945:48065e997df0 43946:ba88bb44c192
   146    str "(" |-- pt --| str "&" -- pt --| str ")" >> RealArith.Branch) input
   146    str "(" |-- pt --| str "&" -- pt --| str ")" >> RealArith.Branch) input
   147   end
   147   end
   148 
   148 
   149 (* scanner *)
   149 (* scanner *)
   150 
   150 
   151 fun cert_to_pss_tree ctxt input_str = Symbol.scanner "bad certificate" (parse_cert_tree ctxt)
   151 fun cert_to_pss_tree ctxt input_str =
   152   (filter_out Symbol.is_blank (Symbol.explode input_str))
   152   Symbol.scanner "Bad certificate" (parse_cert_tree ctxt)
       
   153     (filter_out Symbol.is_blank (Symbol.explode input_str))
   153 
   154 
   154 end
   155 end
   155 
   156 
   156