# HG changeset patch
# User kleing
# Date 1363698293 -3600
# Node ID e1e8191c6725a5c572b37001cb34589c563d284a
# Parent  a5af7c2baf2b1cbff5410b9d1e90793e46d025d6
export datatype definition which gets expanded too much in antiquotation

diff -r a5af7c2baf2b -r e1e8191c6725 src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Tue Mar 19 14:07:13 2013 +0100
+++ b/src/HOL/IMP/Types.thy	Tue Mar 19 14:04:53 2013 +0100
@@ -9,7 +9,9 @@
 type_synonym vname = string
 type_synonym state = "vname \<Rightarrow> val"
 
+text_raw{*\snip{aexptDef}{0}{2}{% *}
 datatype aexp =  Ic int | Rc real | V vname | Plus aexp aexp
+text_raw{*}%endsnip*}
 
 inductive taval :: "aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool" where
 "taval (Ic i) s (Iv i)" |