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 \ state \ bool" where