changeset 68660 | 4ce18f389f53 |
parent 66453 | cc19f7ca2ed6 |
child 69597 | ff784d5a5bfb |
--- a/src/HOL/ex/Computations.thy Wed Jul 18 20:51:22 2018 +0200 +++ b/src/HOL/ex/Computations.thy Wed Jul 18 20:51:23 2018 +0200 @@ -5,7 +5,7 @@ section \<open>Simple example for computations generated by the code generator\<close> theory Computations - imports HOL.Nat HOL.Fun_Def HOL.Num HOL.Code_Numeral + imports Main begin fun even :: "nat \<Rightarrow> bool"