--- a/src/LCF/ex/Ex3.thy Tue Nov 11 11:47:53 2014 +0100 +++ b/src/LCF/ex/Ex3.thy Tue Nov 11 13:40:13 2014 +0100 @@ -1,7 +1,7 @@ section {* Addition with fixpoint of successor *} theory Ex3 -imports LCF +imports "../LCF" begin axiomatization