added header;
authorwenzelm
Thu Apr 26 16:39:11 2007 +0200 (2007-04-26)
changeset 228179dfadec17cc4
parent 22816 0eba117368d9
child 22818 c0695a818c09
added header;
src/HOL/Record.thy
     1.1 --- a/src/HOL/Record.thy	Thu Apr 26 16:39:10 2007 +0200
     1.2 +++ b/src/HOL/Record.thy	Thu Apr 26 16:39:11 2007 +0200
     1.3 @@ -3,6 +3,8 @@
     1.4      Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
     1.5  *)
     1.6  
     1.7 +header {* Extensible records with structural subtyping *}
     1.8 +
     1.9  theory Record
    1.10  imports Product_Type
    1.11  uses ("Tools/record_package.ML")
    1.12 @@ -27,6 +29,7 @@
    1.13  lemma K_record_cong [cong]: "K_record c x = K_record c x"
    1.14    by (rule refl)
    1.15  
    1.16 +
    1.17  subsection {* Concrete record syntax *}
    1.18  
    1.19  nonterminals
    1.20 @@ -64,4 +67,3 @@
    1.21  setup RecordPackage.setup
    1.22  
    1.23  end
    1.24 -