src/HOL/Typedef.thy
changeset 12023 d982f98e0f0d
parent 11982 65e2822d83dd
child 13412 666137b488a4
     1.1 --- a/src/HOL/Typedef.thy	Sat Nov 03 01:33:33 2001 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Sat Nov 03 01:33:54 2001 +0100
     1.3 @@ -8,8 +8,6 @@
     1.4  theory Typedef = Set
     1.5  files ("Tools/typedef_package.ML"):
     1.6  
     1.7 -subsection {* HOL type definitions *}
     1.8 -
     1.9  constdefs
    1.10    type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
    1.11    "type_definition Rep Abs A ==