diff -r d804729d6cf4 -r 6542026b95cd Nominal/Term7.thy
--- a/Nominal/Term7.thy	Tue Mar 23 07:04:27 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-theory Term7
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
-begin
-
-atom_decl name
-
-(* example with a respectful bn function defined over the type itself *)
-
-datatype rtrm7 =
-  rVr7 "name"
-| rLm7 "name" "rtrm7" --"bind left in right"
-| rLt7 "rtrm7" "rtrm7" --"bind (bv7 left) in (right)"
-
-primrec
-  rbv7
-where
-  "rbv7 (rVr7 n) = {atom n}"
-| "rbv7 (rLm7 n t) = rbv7 t - {atom n}"
-| "rbv7 (rLt7 l r) = rbv7 l \<union> rbv7 r"
-
-setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term7.rtrm7") 1 *}
-thm permute_rtrm7.simps
-
-local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term7.rtrm7") [
-  [[[]], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv7}, 0)]]]] *}
-print_theorems
-notation
-  alpha_rtrm7 ("_ \<approx>7a _" [100, 100] 100)
-thm alpha_rtrm7.intros
-thm fv_rtrm7.simps
-inductive
-  alpha7 :: "rtrm7 \<Rightarrow> rtrm7 \<Rightarrow> bool" ("_ \<approx>7 _" [100, 100] 100)
-where
-  a1: "a = b \<Longrightarrow> (rVr7 a) \<approx>7 (rVr7 b)"
-| a2: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha7 fv_rtrm7 pi ({atom b}, s))) \<Longrightarrow> rLm7 a t \<approx>7 rLm7 b s"
-| a3: "(\<exists>pi. (((rbv7 t1), s1) \<approx>gen alpha7 fv_rtrm7 pi ((rbv7 t2), s2))) \<Longrightarrow> rLt7 t1 s1 \<approx>7 rLt7 t2 s2"
-
-lemma "(x::name) \<noteq> y \<Longrightarrow> \<not> (alpha7 ===> op =) rbv7 rbv7"
-  apply simp
-  apply (rule_tac x="rLt7 (rVr7 x) (rVr7 x)" in exI)
-  apply (rule_tac x="rLt7 (rVr7 y) (rVr7 y)" in exI)
-  apply simp
-  apply (rule a3)
-  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alpha_gen fresh_star_def)
-  apply (rule a1)
-  apply (rule refl)
-done
-
-end