--- a/src/Pure/more_thm.ML Sun Feb 25 12:59:08 2018 +0100 +++ b/src/Pure/more_thm.ML Sun Feb 25 15:44:46 2018 +0100 @@ -350,7 +350,7 @@ (** basic derived rules **) (*Elimination of implication - A A ==> B + A A \<Longrightarrow> B ------------ B *)