src/HOL/Nominal/Examples/Fsub.thy
changeset 58305 57752a91eec4
parent 55417 01fbfb60c33e
child 61069 aefe89038dd2
     1.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4    there are infinitely many elements in @{text "tyvrs"} and @{text "vrs"}. *}
     1.5  
     1.6  text{* The constructors for types and terms in System \FSUB{} contain abstractions 
     1.7 -  over type-variables and term-variables. The nominal datatype-package uses 
     1.8 +  over type-variables and term-variables. The nominal datatype package uses 
     1.9    @{text "\<guillemotleft>\<dots>\<guillemotright>\<dots>"} to indicate where abstractions occur. *}
    1.10  
    1.11  nominal_datatype ty =