src/HOL/Library/Function_Division.thy
 changeset 60500 903bb1495239 parent 60429 d3d1e185cd63 child 69593 3dda49e08b9d
```     1.1 --- a/src/HOL/Library/Function_Division.thy	Wed Jun 17 10:57:11 2015 +0200
1.2 +++ b/src/HOL/Library/Function_Division.thy	Wed Jun 17 11:03:05 2015 +0200
1.3 @@ -2,13 +2,13 @@
1.4      Author:     Florian Haftmann, TUM
1.5  *)
1.6
1.7 -section {* Pointwise instantiation of functions to division *}
1.8 +section \<open>Pointwise instantiation of functions to division\<close>
1.9
1.10  theory Function_Division
1.11  imports Function_Algebras
1.12  begin
1.13
1.14 -subsection {* Syntactic with division *}
1.15 +subsection \<open>Syntactic with division\<close>
1.16
1.17  instantiation "fun" :: (type, inverse) inverse
1.18  begin
1.19 @@ -29,12 +29,12 @@
1.20    "(f / g) x = f x / g x"
1.22
1.23 -text {*
1.24 +text \<open>
1.25    Unfortunately, we cannot lift this operations to algebraic type
1.26    classes for division: being different from the constant
1.27    zero function @{term "f \<noteq> 0"} is too weak as precondition.
1.28    So we must introduce our own set of lemmas.
1.29 -*}
1.30 +\<close>
1.31
1.32  abbreviation zero_free :: "('b \<Rightarrow> 'a::field) \<Rightarrow> bool" where
1.33    "zero_free f \<equiv> \<not> (\<exists>x. f x = 0)"
1.34 @@ -54,12 +54,12 @@
1.35    shows "f / g = f * inverse g"
1.36    by (simp add: fun_eq_iff divide_inverse)
1.37
1.38 -text {* Feel free to extend this. *}
1.39 +text \<open>Feel free to extend this.\<close>
1.40
1.41 -text {*
1.42 +text \<open>
1.43    Another possibility would be a reformulation of the division type
1.44    classes to user a @{term zero_free} predicate rather than
1.45    a direct @{term "a \<noteq> 0"} condition.
1.46 -*}
1.47 +\<close>
1.48
1.49  end
```