author | haftmann |
Mon, 16 Feb 2009 19:11:16 +0100 | |
changeset 29938 | a0e54cf21fd4 |
parent 29937 | ffed4bd4bfad |
child 29939 | 2138ff0ec94a |
--- a/src/HOL/ex/Efficient_Nat_examples.thy Mon Feb 16 19:11:16 2009 +0100 +++ b/src/HOL/ex/Efficient_Nat_examples.thy Mon Feb 16 19:11:16 2009 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/ex/Efficient_Nat_examples.thy - ID: $Id$ Author: Florian Haftmann, TU Muenchen *) header {* Simple examples for Efficient\_Nat theory. *} theory Efficient_Nat_examples -imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat +imports Complex_Main Efficient_Nat begin fun to_n :: "nat \<Rightarrow> nat list" where