# HG changeset patch
# User blanchet
# Date 1458646777 -3600
# Node ID b287b56a6ce556194a31f22bd3245823985387be
# Parent  f50d7efc8fe35fb8505d244b11afc7117ddd4562
file header

diff -r f50d7efc8fe3 -r b287b56a6ce5 src/HOL/Datatype_Examples/Lift_BNF.thy
--- a/src/HOL/Datatype_Examples/Lift_BNF.thy	Tue Mar 22 12:39:37 2016 +0100
+++ b/src/HOL/Datatype_Examples/Lift_BNF.thy	Tue Mar 22 12:39:37 2016 +0100
@@ -1,3 +1,12 @@
+(*  Title:      HOL/Datatype_Examples/Lift_BNF.thy
+    Author:     Dmitriy Traytel, ETH Zürich
+    Copyright   2015
+
+Demonstration of the "lift_bnf" command.
+*)
+
+section {* Demonstration of the @{command lift_bnf} Command *}
+
 theory Lift_BNF
 imports Main
 begin