file header
authorblanchet
Tue Mar 22 12:39:37 2016 +0100 (2016-03-22)
changeset 62695b287b56a6ce5
parent 62694 f50d7efc8fe3
child 62696 7325d8573fb8
file header
src/HOL/Datatype_Examples/Lift_BNF.thy
     1.1 --- a/src/HOL/Datatype_Examples/Lift_BNF.thy	Tue Mar 22 12:39:37 2016 +0100
     1.2 +++ b/src/HOL/Datatype_Examples/Lift_BNF.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -1,3 +1,12 @@
     1.4 +(*  Title:      HOL/Datatype_Examples/Lift_BNF.thy
     1.5 +    Author:     Dmitriy Traytel, ETH Z├╝rich
     1.6 +    Copyright   2015
     1.7 +
     1.8 +Demonstration of the "lift_bnf" command.
     1.9 +*)
    1.10 +
    1.11 +section {* Demonstration of the @{command lift_bnf} Command *}
    1.12 +
    1.13  theory Lift_BNF
    1.14  imports Main
    1.15  begin