diff -r 9e247b9505f0 -r 2605ea41bbdd Quot/Examples/Terms.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/Terms.thy	Thu Jan 14 12:14:35 2010 +0100
@@ -0,0 +1,37 @@
+theory Terms
+imports Nominal "../QuotMain" "../QuotList"
+begin
+
+atom_decl name
+
+(* lets with binding patterns *)
+datatype trm1 =
+  Vr1 "name"
+| Ap1 "trm1" "trm1"
+| Lm1 "name" "trm1"
+| Lt1 "bp" "trm1" "trm1"
+and bp =
+  BUnit
+| BVr "name"
+| BPr "bp" "bp"
+
+(* lets with single assignments *)
+datatype trm2 =
+  Vr2 "name"
+| Ap2 "trm2" "trm2"
+| Lm2 "name" "trm2"
+| Lt2 "assign" "trm2"
+and assign =
+  As "name" "trm2"
+
+
+(* lets with many assignments *)
+datatype trm3 =
+  Vr3 "name"
+| Ap3 "trm3" "trm3"
+| Lm3 "name" "trm3"
+| Lt3 "assign" "trm3"
+and assigns =
+  ANil
+| ACons "name" "trm3" "assigns"
+