# HG changeset patch
# User nipkow
# Date 1387786898 -3600
# Node ID bf86b2002c969c2d1f0acbb4a7990169dafa1862
# Parent  10df188349b318caeb482d4979561a515c18aa8f
tuned

diff -r 10df188349b3 -r bf86b2002c96 src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Sat Dec 21 09:44:30 2013 +0100
+++ b/src/HOL/IMP/BExp.thy	Mon Dec 23 09:21:38 2013 +0100
@@ -2,9 +2,7 @@
 
 subsection "Boolean Expressions"
 
-text_raw{*\snip{BExpbexpdef}{0}{1}{% *}
 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
-text_raw{*}%endsnip*}
 
 text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where