diff -r cfda1ec86a9e -r b2efe803f1da Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Apr 19 09:25:55 2010 +0200
+++ b/Nominal/Parser.thy	Mon Apr 19 10:00:52 2010 +0200
@@ -293,31 +293,49 @@
 ML {* val cheat_const_rsp = Unsynchronized.ref false *}
 
 (* nominal_datatype2 does the following things in order:
+
+Parser.thy/raw_nominal_decls
   1) define the raw datatype
   2) define the raw binding functions
+Perm.thy/define_raw_perms
   3) define permutations of the raw datatype and show that raw type is in the pt typeclass
-  4) define fv and fb_bn
+Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
+  4) define fv and fv_bn
   5) define alpha and alpha_bn
+Perm.thy/distinct_rel
   6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
+Tacs.thy/build_rel_inj
   6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
      (left-to-right by intro rule, right-to-left by cases; simp)
+Equivp.thy/prove_eqvt
   7) prove bn_eqvt (common induction on the raw datatype)
   8) prove fv_eqvt (common induction on the raw datatype with help of above)
+Rsp.thy/build_alpha_eqvts
   9) prove alpha_eqvt and alpha_bn_eqvt
      (common alpha-induction, unfolding alpha_gen, permute of #* and =)
+Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps
  10) prove that alpha and alpha_bn are equivalence relations
      (common induction and application of 'compose' lemmas)
+Lift.thy/define_quotient_types
  11) define quotient types
+Rsp.thy/build_fvbv_rsps
  12) prove bn respects     (common induction and simp with alpha_gen)
+Rsp.thy/prove_const_rsp
  13) prove fv respects     (common induction and simp with alpha_gen)
  14) prove permute respects    (unfolds to alpha_eqvt)
+Rsp.thy/prove_alpha_bn_rsp
  15) prove alpha_bn respects
      (alpha_induct then cases then sym and trans of the relations)
+Rsp.thy/prove_alpha_alphabn
  16) show that alpha implies alpha_bn (by unduction, needed in following step)
+Rsp.thy/prove_const_rsp
  17) prove respects for all datatype constructors
      (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
+Lift.thy/quotient_lift_consts_export
  18) define lifted constructors, fv, bn, alpha_bn, permutations
+Perm.thy/define_lifted_perms
  19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
+Lift.thy/lift_thm
  20) lift permutation simplifications
  21) lift induction
  22) lift fv
@@ -325,8 +343,11 @@
  24) lift eq_iff
  25) lift alpha_distincts
  26) lift fv and bn eqvts
+Equivp.thy/prove_supports
  27) prove that union of arguments supports constructors
+Equivp.thy/prove_fs
  28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
+Equivp.thy/supp_eq
  29) prove supp = fv
 *)
 ML {*