--- a/Nominal/Test.thy Tue Mar 23 08:22:48 2010 +0100
+++ b/Nominal/Test.thy Tue Mar 23 08:33:48 2010 +0100
@@ -108,30 +108,8 @@
thm trm0_pat0.distinct
thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
-text {* example type schemes *}
-
-nominal_datatype t =
- VarTS "name"
-| FunTS "t" "t"
-and tyS =
- All xs::"name fset" ty::"t" bind xs in ty
-
-thm t_tyS.fv
-thm t_tyS.eq_iff
-thm t_tyS.bn
-thm t_tyS.perm
-thm t_tyS.induct
-thm t_tyS.distinct
-thm t_tyS.fv[simplified t_tyS.supp]
-
-ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
-ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}
-
-
-
(* example 1 from Terms.thy *)
-
nominal_datatype trm1 =
Vr1 "name"
| Ap1 "trm1" "trm1"
@@ -266,28 +244,6 @@
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
-
-(* example from my PHD *)
-
-atom_decl coname
-
-nominal_datatype phd =
- Ax "name" "coname"
-| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2
-| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2
-| AndL1 n::"name" t::"phd" "name" bind n in t
-| AndL2 n::"name" t::"phd" "name" bind n in t
-| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2
-| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t
-
-thm phd.fv
-thm phd.eq_iff
-thm phd.bn
-thm phd.perm
-thm phd.induct
-thm phd.distinct
-thm phd.fv[simplified phd.supp]
-
(* example 3 from Peter Sewell's bestiary *)
nominal_datatype exp =
@@ -471,18 +427,6 @@
"bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
*)
-text {* weirdo example from Peter Sewell's bestiary *}
-
-nominal_datatype weird =
- WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
- bind x in p1, bind x in p2, bind y in p2, bind y in p3
-| WV "name"
-| WP "weird" "weird"
-
-thm permute_weird_raw.simps[no_vars]
-thm alpha_weird_raw.intros[no_vars]
-thm fv_weird_raw.simps[no_vars]
-
(* example 8 from Terms.thy *)
(* Binding in a term under a bn, needs to fail *)