src/HOL/Decision_Procs/approximation_generator.ML
changeset 59582 0fbed69ff081
parent 58988 6ebf918128b9
child 59621 291934bac95e
equal deleted inserted replaced
59580:cbc38731d42f 59582:0fbed69ff081
   115     "int_of_integer (- 1) = - 1"
   115     "int_of_integer (- 1) = - 1"
   116     by auto
   116     by auto
   117   }
   117   }
   118 
   118 
   119 fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
   119 fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
   120 fun conv_term thy conv r = cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
   120 fun conv_term thy conv r = Thm.cterm_of thy r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
   121 
   121 
   122 fun approx_random ctxt prec eps frees e xs genuine_only size seed =
   122 fun approx_random ctxt prec eps frees e xs genuine_only size seed =
   123   let
   123   let
   124     val (rs, seed') = random_float_list size xs seed
   124     val (rs, seed') = random_float_list size xs seed
   125     fun mk_approx_form e ts =
   125     fun mk_approx_form e ts =