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