src/FOL/ex/Locale_Test/Locale_Test1.thy
changeset 67119 acb0807ddb56
parent 62020 5d208fd2507d
child 67347 bf269672c203
     1.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sat Dec 02 16:50:53 2017 +0000
     1.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Sun Dec 03 13:22:09 2017 +0100
     1.3 @@ -726,7 +726,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -sublocale lgrp < "def"?: dgrp
     1.8 +sublocale lgrp < def?: dgrp
     1.9    rewrites one_equation: "dgrp.one(prod) = one" and inv_equation: "dgrp.inv(prod, x) = inv(x)"
    1.10  proof -
    1.11    show "dgrp(prod)" by unfold_locales