src/HOL/ex/Computations.thy
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"