diff -r 93aaff2b0ae0 -r 40c36a4aee1f src/HOL/ex/Computations.thy
--- a/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:32 2017 +0100
+++ b/src/HOL/ex/Computations.thy	Mon Feb 06 20:56:33 2017 +0100
@@ -36,9 +36,11 @@
   (fn post => post o HOLogic.mk_nat o int_of_nat o the);
 
 val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies
-  HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool }
+  HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool}
   (K the);
 
+val comp_check = @{computation_check Trueprop};
+
 end
 \<close>
 
@@ -55,6 +57,10 @@
 \<close>
 
 ML_val \<open>
+  comp_check @{context} @{cprop "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 > fib (Suc (Suc 0))"}
+\<close>
+  
+ML_val \<open>
   comp_numeral @{context} @{term "Suc 42 + 7"}
   |> Syntax.string_of_term @{context}
   |> writeln