src/HOL/Quotient.thy
changeset 67091 1393c2340eec
parent 63343 fb5d8a50c641
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Quotient.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4    by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI)
     1.5  
     1.6  lemma abs_o_rep:
     1.7 -  "Abs o Rep = id"
     1.8 +  "Abs \<circ> Rep = id"
     1.9    unfolding fun_eq_iff
    1.10    by (simp add: Quotient3_abs_rep)
    1.11  
    1.12 @@ -280,25 +280,25 @@
    1.13  
    1.14  (* Next four lemmas are unused *)
    1.15  lemma all_reg:
    1.16 -  assumes a: "!x :: 'a. (P x --> Q x)"
    1.17 +  assumes a: "\<forall>x :: 'a. (P x \<longrightarrow> Q x)"
    1.18    and     b: "All P"
    1.19    shows "All Q"
    1.20    using a b by fast
    1.21  
    1.22  lemma ex_reg:
    1.23 -  assumes a: "!x :: 'a. (P x --> Q x)"
    1.24 +  assumes a: "\<forall>x :: 'a. (P x \<longrightarrow> Q x)"
    1.25    and     b: "Ex P"
    1.26    shows "Ex Q"
    1.27    using a b by fast
    1.28  
    1.29  lemma ball_reg:
    1.30 -  assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
    1.31 +  assumes a: "\<forall>x :: 'a. (x \<in> R \<longrightarrow> P x \<longrightarrow> Q x)"
    1.32    and     b: "Ball R P"
    1.33    shows "Ball R Q"
    1.34    using a b by fast
    1.35  
    1.36  lemma bex_reg:
    1.37 -  assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
    1.38 +  assumes a: "\<forall>x :: 'a. (x \<in> R \<longrightarrow> P x \<longrightarrow> Q x)"
    1.39    and     b: "Bex R P"
    1.40    shows "Bex R Q"
    1.41    using a b by fast