--- a/src/HOL/Eisbach/Eisbach.thy Mon Jan 11 15:58:18 2016 +1100 +++ b/src/HOL/Eisbach/Eisbach.thy Tue Jan 12 11:00:55 2016 +1100 @@ -5,7 +5,7 @@ *) theory Eisbach -imports Main +imports Pure keywords "method" :: thy_decl and "conclusion"