src/HOL/Library/OptionalSugar.thy
changeset 15476 b8cb20cc0c0b
parent 15469 f5d22f504ab9
child 19674 22b635240905
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Thu Jan 27 12:37:02 2005 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Thu Jan 27 13:33:21 2005 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Gerwin Klain, Tobias Nipkow
     1.5      Copyright   2005 NICTA and TUM
     1.6  *)
     1.7 -
     1.8 +(*<*)
     1.9  theory OptionalSugar
    1.10  imports LaTeXsugar
    1.11  begin
    1.12 @@ -34,4 +34,5 @@
    1.13    "_bind (DUMMY#p) e" <= "_bind p (tl e)"
    1.14  
    1.15  
    1.16 -end
    1.17 \ No newline at end of file
    1.18 +end
    1.19 +(*>*)