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.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
```