# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269330404 -3600
# Node ID 2406350c358f5cfc369e1816bd3793a9fbd229f9
# Parent  af34dd3418fe7dacf4e0b1dd9ec327cafa33ea66
Term1 is identical to Example 3

diff -r af34dd3418fe -r 2406350c358f Nominal/Ex3.thy
--- a/Nominal/Ex3.thy	Tue Mar 23 08:45:08 2010 +0100
+++ b/Nominal/Ex3.thy	Tue Mar 23 08:46:44 2010 +0100
@@ -2,6 +2,8 @@
 imports "Parser"
 begin
 
+(* Example 3, identical to example 1 from Terms.thy *)
+
 atom_decl name
 
 ML {* val _ = recursive := false  *}
diff -r af34dd3418fe -r 2406350c358f Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 23 08:45:08 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 08:46:44 2010 +0100
@@ -6,32 +6,6 @@
 
 ML {* val _ = recursive := false  *}
 
-(* example 1 from Terms.thy *)
-
-nominal_datatype trm1 =
-  Vr1 "name"
-| Ap1 "trm1" "trm1"
-| Lm1 x::"name" t::"trm1"       bind x in t
-| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t
-and bp1 =
-  BUnit1
-| BV1 "name"
-| BP1 "bp1" "bp1"
-binder
-  bv1
-where
-  "bv1 (BUnit1) = {}"
-| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
-| "bv1 (BV1 x) = {atom x}"
-
-thm trm1_bp1.fv
-thm trm1_bp1.eq_iff
-thm trm1_bp1.bn
-thm trm1_bp1.perm
-thm trm1_bp1.induct
-thm trm1_bp1.distinct
-thm trm1_bp1.fv[simplified trm1_bp1.supp]
-
 text {* example 3 from Terms.thy *}
 
 nominal_datatype trm3 =