--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Nov 06 08:11:58 2009 +0100
@@ -121,7 +121,8 @@
skip_proof = chk "skip_proof",
inductify = chk "inductify",
random = chk "random",
- depth_limited = chk "depth_limited"
+ depth_limited = chk "depth_limited",
+ annotated = chk "annotated"
}
end
@@ -149,7 +150,8 @@
val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup
val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
- "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited"]
+ "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited",
+ "annotated"]
local structure P = OuterParse
in