changeset 49834 | b27bbb021df1 |
parent 49812 | e3945ddcb9aa |
child 49836 | c13b39542972 |
--- a/src/Doc/IsarRef/HOL_Specific.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/Doc/IsarRef/HOL_Specific.thy Fri Oct 12 18:58:20 2012 +0200 @@ -1189,7 +1189,7 @@ \medskip The following trivial example pulls a three-element type into existence within the formal logical environment of HOL. *} -typedef (open) three = "{(True, True), (True, False), (False, True)}" +typedef three = "{(True, True), (True, False), (False, True)}" by blast definition "One = Abs_three (True, True)"