# HG changeset patch # User wenzelm # Date 1213200071 -7200 # Node ID bd387c1a05368d934fd2d1b944ede9ca9fffb611 # Parent a42aef558ce3e5410fab12c4799daf5d489664bc removed obsolete/unused pred_congs; diff -r a42aef558ce3 -r bd387c1a0536 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Wed Jun 11 15:41:57 2008 +0200 +++ b/src/FOL/IFOL.thy Wed Jun 11 18:01:11 2008 +0200 @@ -518,16 +518,6 @@ apply assumption done -(*special cases for free variables P, Q, R, S -- up to 3 arguments*) - -ML {* -bind_thms ("pred_congs", - List.concat (map (fn c => - map (fn th => read_instantiate [("P",c)] th) - [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}]) - (explode"PQRS"))) -*} - (*special case for the equality predicate!*) lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'" apply (erule (1) pred2_cong)