tuned
authornipkow
Mon, 23 Dec 2013 09:21:38 +0100
changeset 54846 bf86b2002c96
parent 54845 10df188349b3
child 54847 d6cf9a5b9be9
child 54851 48a24d371ebb
tuned
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