tuned comments;
authorwenzelm
Wed Jun 11 15:41:57 2008 +0200 (2008-06-11)
changeset 27150a42aef558ce3
parent 27149 123377499a8e
child 27151 bd387c1a0536
tuned comments;
src/FOL/IFOL.thy
src/FOLP/IFOLP.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/func.thy
     1.1 --- a/src/FOL/IFOL.thy	Wed Jun 11 15:41:33 2008 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Wed Jun 11 15:41:57 2008 +0200
     1.3 @@ -226,9 +226,7 @@
     1.4    done
     1.5  
     1.6  (* For substitution into an assumption P, reduce Q to P-->Q, substitute into
     1.7 -   this implication, then apply impI to move P back into the assumptions.
     1.8 -   To specify P use something like
     1.9 -      eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
    1.10 +   this implication, then apply impI to move P back into the assumptions.*)
    1.11  lemma rev_mp: "[| P;  P --> Q |] ==> Q"
    1.12    by (erule mp)
    1.13  
     2.1 --- a/src/FOLP/IFOLP.thy	Wed Jun 11 15:41:33 2008 +0200
     2.2 +++ b/src/FOLP/IFOLP.thy	Wed Jun 11 15:41:57 2008 +0200
     2.3 @@ -216,9 +216,7 @@
     2.4    done
     2.5  
     2.6  (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
     2.7 -   this implication, then apply impI to move P back into the assumptions.
     2.8 -   To specify P use something like
     2.9 -      eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
    2.10 +   this implication, then apply impI to move P back into the assumptions.*)
    2.11  lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
    2.12    apply (assumption | rule mp)+
    2.13    done
     3.1 --- a/src/ZF/AC/WO6_WO1.thy	Wed Jun 11 15:41:33 2008 +0200
     3.2 +++ b/src/ZF/AC/WO6_WO1.thy	Wed Jun 11 15:41:57 2008 +0200
     3.3 @@ -395,8 +395,6 @@
     3.4  apply (erule succ_natD)
     3.5  apply (rule_tac x = "a++a" in exI)
     3.6  apply (rule_tac x = "gg2 (f,a,b,x) " in exI)
     3.7 -(*Calling fast_tac might get rid of the res_inst_tac calls, but it
     3.8 -  is just too slow.*)
     3.9  apply (simp add: Ord_oadd domain_gg2 UN_gg2_eq gg2_lepoll_m)
    3.10  done
    3.11  
     4.1 --- a/src/ZF/func.thy	Wed Jun 11 15:41:33 2008 +0200
     4.2 +++ b/src/ZF/func.thy	Wed Jun 11 15:41:57 2008 +0200
     4.3 @@ -90,7 +90,7 @@
     4.4  apply (blast intro: function_apply_Pair)
     4.5  done
     4.6  
     4.7 -(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
     4.8 +(*Conclusion is flexible -- use rule_tac or else apply_funtype below!*)
     4.9  lemma apply_type [TC]: "[| f: Pi(A,B);  a:A |] ==> f`a : B(a)"
    4.10  by (blast intro: apply_Pair dest: fun_is_rel)
    4.11