--- a/src/HOL/Decision_Procs/approximation_generator.ML Mon Mar 30 00:13:37 2015 +0200
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Mon Mar 30 10:52:54 2015 +0200
@@ -141,7 +141,7 @@
#> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
frees
in
- if approximate ctxt (mk_approx_form e ts) |> is_True
+ if Approximation.approximate ctxt (mk_approx_form e ts) |> is_True
then SOME (true, ts')
else (if genuine_only then NONE else SOME (false, ts'))
end
@@ -161,6 +161,8 @@
"\<not> \<not> q \<longleftrightarrow> q"
by auto}
+val form_equations = @{thms interpret_form_equations};
+
fun reify_goal ctxt t =
HOLogic.mk_not t
|> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)