tuned;
authorwenzelm
Sat Oct 13 21:43:00 2001 +0200 (2001-10-13)
changeset 11743b9739c85dd44
parent 11742 44034a6474e5
child 11744 3a4625eaead0
tuned;
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/Typedef.thy	Sat Oct 13 20:32:38 2001 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Sat Oct 13 21:43:00 2001 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4  (*  Title:      HOL/Typedef.thy
     1.5      ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Munich
     1.7 +*)
     1.8  
     1.9 -Misc set-theory lemmas and HOL type definitions.
    1.10 -*)
    1.11 +header {* Set-theory lemmas and HOL type definitions *}
    1.12  
    1.13  theory Typedef = Set
    1.14  files "subset.ML" "equalities.ML" "mono.ML" ("Tools/typedef_package.ML"):
    1.15 @@ -24,7 +24,7 @@
    1.16  setup Rulify.setup
    1.17  
    1.18  
    1.19 -section {* HOL type definitions *}
    1.20 +subsection {* HOL type definitions *}
    1.21  
    1.22  constdefs
    1.23    type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"