# HG changeset patch # User steckerm # Date 1411202664 -7200 # Node ID 111d801b5d5d795274c05f2d3eb225bc16505814 # Parent 539cc471186f0ddddd213274c1a62d5cddceab06 Changed proof method to auto for custom Waldmeister lemma diff -r 539cc471186f -r 111d801b5d5d src/HOL/ATP.thy --- a/src/HOL/ATP.thy Sat Sep 20 10:44:24 2014 +0200 +++ b/src/HOL/ATP.thy Sat Sep 20 10:44:24 2014 +0200 @@ -138,7 +138,7 @@ by simp lemma boolean_comm: "(P \ Q) = (Q \ P)" - by metis + by auto lemmas waldmeister_fol = boolean_equality boolean_comm simp_thms(1-5,7-8,11-25,27-33) disj_comms disj_assoc conj_comms conj_assoc