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.21    by (simp add: divide_fun_def)
    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