| changeset 8922 | 490637ba1d7f |
| parent 8920 | af5e09b6c208 |
| child 9363 | 86b48eafc70d |
--- a/src/HOL/AxClasses/Tutorial/Group.thy Mon May 22 16:03:43 2000 +0200 +++ b/src/HOL/AxClasses/Tutorial/Group.thy Mon May 22 16:04:32 2000 +0200 @@ -92,7 +92,7 @@ qed; -subsection {* Concrete instantiation \label{sec:inst-arity} *}; +subsection {* Concrete instantiation *}; defs times_bool_def: "x [*] y == x ~= (y::bool)"