# HG changeset patch
# User blanchet
# Date 1458649960 -3600
# Node ID 84a302ab9147c2260c5fb0c265d1914cca2b5f48
# Parent  7325d8573fb87f0d61f0891eee958c00efcfbae6
compile

diff -r 7325d8573fb8 -r 84a302ab9147 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 13:32:40 2016 +0100
@@ -5,7 +5,7 @@
 Demonstration of the "lift_bnf" command.
 *)
 
-section {* Demonstration of the @{command lift_bnf} Command *}
+section {* Demonstration of the \textbf{lift_bnf} Command *}
 
 theory Lift_BNF
 imports Main