# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263467859 -3600
# Node ID f14e41e9b08faafcc7ebb182da744036c15cdd69
# Parent  2605ea41bbddd384bd089fd547ddcca569996bad# Parent  4163fe3dbf8c976d75bf0bd9076b8654eac55987
merged

diff -r 4163fe3dbf8c -r f14e41e9b08f Quot/Examples/Terms.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/Terms.thy	Thu Jan 14 12:17:39 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"
+