--- a/ProgTutorial/Package/Ind_Prelims.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Tue May 14 11:10:53 2019 +0200
@@ -169,7 +169,7 @@
 apply(unfold trcl_def)
 apply(blast)
 done
-
+term "even"
 text {*
   Experience has shown that it is generally a bad idea to rely heavily on
   @{text blast}, @{text auto} and the like in automated proofs. The reason is
@@ -194,7 +194,10 @@
   below @{text "P"} and @{text "Q"}).
 *}
 
-definition "even \<equiv> 
+hide_const even
+hide_const odd
+
+definition "even \<equiv>
   \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
                  \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"