changeset 24136 | 0c6c943d8f1e |
parent 24128 | 654b3a988f6a |
child 24300 | e170cee91c66 |
--- a/src/HOL/ex/Meson_Test.thy Thu Aug 02 22:43:47 2007 +0200 +++ b/src/HOL/ex/Meson_Test.thy Thu Aug 02 23:18:13 2007 +0200 @@ -86,6 +86,8 @@ by (best_prolog_tac size_of_subgoals horns43); (*1.6 secs*) *} +ML {* Logic.auto_rename := false; *} + (* #1 (q x xa ==> ~ q x xa) ==> q xa x #2 (q xa x ==> ~ q xa x) ==> q x xa