tuned;
authorwenzelm
Sun Nov 20 13:29:12 2011 +0100 (2011-11-20)
changeset 45594d320f2f9f331
parent 45593 7247ade03aa9
child 45595 fe57d786fd5b
tuned;
src/FOL/FOL.thy
src/FOLP/IFOLP.thy
     1.1 --- a/src/FOL/FOL.thy	Sat Nov 19 21:23:16 2011 +0100
     1.2 +++ b/src/FOL/FOL.thy	Sun Nov 20 13:29:12 2011 +0100
     1.3 @@ -408,7 +408,7 @@
     1.4    unfolding atomize_conj induct_conj_def .
     1.5  
     1.6  lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
     1.7 -lemmas induct_rulify [symmetric, standard] = induct_atomize
     1.8 +lemmas induct_rulify [symmetric] = induct_atomize
     1.9  lemmas induct_rulify_fallback =
    1.10    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.11  
     2.1 --- a/src/FOLP/IFOLP.thy	Sat Nov 19 21:23:16 2011 +0100
     2.2 +++ b/src/FOLP/IFOLP.thy	Sun Nov 20 13:29:12 2011 +0100
     2.3 @@ -435,8 +435,11 @@
     2.4    apply (erule sym)
     2.5    done
     2.6  
     2.7 -(*calling "standard" reduces maxidx to 0*)
     2.8 -lemmas ssubst = sym [THEN subst, standard]
     2.9 +schematic_lemma ssubst: "p:b=a \<Longrightarrow> q:P(a) \<Longrightarrow> ?p:P(b)"
    2.10 +  apply (drule sym)
    2.11 +  apply (erule subst)
    2.12 +  apply assumption
    2.13 +  done
    2.14  
    2.15  (*A special case of ex1E that would otherwise need quantifier expansion*)
    2.16  schematic_lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"