--- a/src/Sequents/LK/Quantifiers.thy Sat Feb 01 17:56:03 2014 +0100 +++ b/src/Sequents/LK/Quantifiers.thy Sat Feb 01 18:00:28 2014 +0100 @@ -6,7 +6,7 @@ *) theory Quantifiers -imports LK +imports "../LK" begin lemma "|- (ALL x. P) <-> P"