--- a/src/HOL/Fields.thy Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Fields.thy Wed Oct 29 19:01:49 2014 +0100
@@ -23,8 +23,7 @@
fixes inverse :: "'a \<Rightarrow> 'a"
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-setup {* Sign.add_const_constraint
- (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
context semiring
@@ -47,8 +46,7 @@
end
-setup {* Sign.add_const_constraint
- (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}