diff -r bd40c5cb803d -r d900d19931fa Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Thu Feb 18 11:28:20 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 12:06:59 2010 +0100
@@ -103,30 +103,15 @@
 quotient_type trm1 = rtrm1 / alpha1
   by (rule alpha1_equivp)
 
-quotient_definition
-  "Vr1 :: name \<Rightarrow> trm1"
-is
-  "rVr1"
-
-quotient_definition
-  "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
-  "rAp1"
-
-quotient_definition
-  "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
-  "rLm1"
-
-quotient_definition
-  "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
-  "rLt1"
-
-quotient_definition
-  "fv_trm1 :: trm1 \<Rightarrow> atom set"
-is
-  "fv_rtrm1"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1})))
+*}
+print_theorems
 
 lemma alpha_rfv1:
   shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
@@ -317,6 +302,17 @@
   assign = rassign / alpha2a
   by (auto intro: alpha2_equivp)
 
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2})))
+*}
+print_theorems
 
 
 section {*** lets with many assignments ***}
@@ -495,45 +491,18 @@
   lts = rlts / alphalts
   by (auto intro: alpha5_equivps)
 
-quotient_definition
-  "Vr5 :: name \<Rightarrow> trm5"
-is
-  "rVr5"
-
-quotient_definition
-  "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
-  "rAp5"
-
-quotient_definition
-  "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"
-is
-  "rLt5"
-
-quotient_definition
-  "Lnil :: lts"
-is
-  "rLnil"
-
-quotient_definition
-  "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"
-is
-  "rLcons"
-
-quotient_definition
-   "fv_trm5 :: trm5 \<Rightarrow> atom set"
-is
-  "fv_rtrm5"
-
-quotient_definition
-   "fv_lts :: lts \<Rightarrow> atom set"
-is
-  "fv_rlts"
-
-quotient_definition
-   "bv5 :: lts \<Rightarrow> atom set"
-is
-  "rbv5"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})))
+*}
+print_theorems
 
 lemma rbv5_eqvt:
   "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"
@@ -754,30 +723,15 @@
   trm6 = rtrm6 / alpha6
   by (auto intro: alpha6_equivps)
 
-quotient_definition
-  "Vr6 :: name \<Rightarrow> trm6"
-is
-  "rVr6"
-
-quotient_definition
-  "Lm6 :: name \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
-  "rLm6"
-
-quotient_definition
-  "Lt6 :: trm6 \<Rightarrow> trm6 \<Rightarrow> trm6"
-is
-  "rLt6"
-
-quotient_definition
-   "fv_trm6 :: trm6 \<Rightarrow> atom set"
-is
-  "fv_rtrm6"
-
-quotient_definition
-   "bv6 :: trm6 \<Rightarrow> atom set"
-is
-  "rbv6"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("Vr6", @{term rVr6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lm6", @{term rLm6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("Lt6", @{term rLt6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_trm6", @{term fv_rtrm6}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv6", @{term rbv6})))
+*}
+print_theorems
 
 lemma [quot_respect]:
   "(op = ===> alpha6 ===> alpha6) permute permute"
@@ -785,7 +739,6 @@
 sorry
 
 (* Definitely not true , see lemma below *)
-
 lemma [quot_respect]:"(alpha6 ===> op =) rbv6 rbv6"
 apply simp apply clarify
 apply (erule alpha6.induct)
@@ -1008,35 +961,16 @@
   lam9 = rlam9 / alpha9l and bla9 = rbla9 / alpha9b
 sorry
 
-quotient_definition
-  "qVar9 :: name \<Rightarrow> lam9"
-is
-  "Var9"
-
-quotient_definition
-  "qLam :: name \<Rightarrow> lam9 \<Rightarrow> lam9"
-is
-  "Lam9"
-
-quotient_definition
-  "qBla9 :: lam9 \<Rightarrow> lam9 \<Rightarrow> bla9"
-is
-  "Bla9"
-
-quotient_definition
-  "fv_lam9 :: lam9 \<Rightarrow> atom set"
-is
-  "fv_rlam9"
-
-quotient_definition
-  "fv_bla9 :: bla9 \<Rightarrow> atom set"
-is
-  "fv_rbla9"
-
-quotient_definition
-  "bv9 :: lam9 \<Rightarrow> atom set"
-is
-  "rbv9"
+local_setup {*
+(fn ctxt => ctxt
+ |> snd o (Quotient_Def.quotient_lift_const ("qVar9", @{term Var9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("qLam9", @{term Lam9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("qBla9", @{term Bla9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_lam9", @{term fv_rlam9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("fv_bla9", @{term fv_rbla9}))
+ |> snd o (Quotient_Def.quotient_lift_const ("bv9", @{term rbv9})))
+*}
+print_theorems
 
 instantiation lam9 and bla9 :: pt
 begin