changeset 69216 | 1a52baa70aed |
parent 64290 | fb5c74a58796 |
child 69593 | 3dda49e08b9d |
--- a/src/HOL/Groups.thy Wed Oct 31 15:50:45 2018 +0100 +++ b/src/HOL/Groups.thy Wed Oct 31 15:53:32 2018 +0100 @@ -182,7 +182,7 @@ Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $ Syntax_Phases.term_of_typ ctxt T else raise Match); - in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; + in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end \<close> \<comment> \<open>show types that are presumably too general\<close> class plus =