# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272402700 -7200
# Node ID 209ee65b2395b00fbb1d10db40052fea9d9afffb
# Parent  0c9ef14e9ba4e4efd71569c80c79a29e2ccb8cf2
added some further problemetic tests

diff -r 0c9ef14e9ba4 -r 209ee65b2395 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Apr 27 22:45:50 2010 +0200
+++ b/Nominal/NewParser.thy	Tue Apr 27 23:11:40 2010 +0200
@@ -504,6 +504,20 @@
 thm fv_exp_raw.simps fv_fnclause_raw.simps fv_fnclauses_raw.simps fv_lrb_raw.simps fv_lrbs_raw.simps fv_pat_raw.simps fv_b_lrbs_raw.simps fv_b_pat_raw.simps fv_b_fnclauses_raw.simps fv_b_lrb_raw.simps fv_b_fnclause_raw.simps
 
 
+(* some further tests *)
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam list"
+| Lam x::"name" t::"lam" bind x in t
+
+nominal_datatype ty =
+  Var "name"
+| Fun "ty" "ty"
+
+nominal_datatype tys =
+  All xs::"name fset" ty::"ty_raw" bind xs in ty
+
 
 
 end