src/HOL/Integ/NatSimprocs.thy
changeset 17472 bcbf48d59059
parent 17149 e2b19c92ef51
child 18624 2e7afae14fa5
     1.1 --- a/src/HOL/Integ/NatSimprocs.thy	Sat Sep 17 18:24:57 2005 +0200
     1.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Sat Sep 17 18:25:11 2005 +0200
     1.3 @@ -346,7 +346,7 @@
     1.4    divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
     1.5    le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1
     1.6  
     1.7 -subsubsection{*Division By @{term "-1"}*}
     1.8 +subsubsection{*Division By @{text "-1"}*}
     1.9  
    1.10  lemma divide_minus1 [simp]:
    1.11       "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"