--- a/Nominal/Ex/Lambda.thy	Sun Aug 22 14:02:49 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Wed Aug 25 09:02:06 2010 +0800
@@ -3,14 +3,104 @@
 begin
 
 atom_decl name
-declare [[STEPS = 2]]
+declare [[STEPS = 20]]
 
-nominal_datatype 'a lam =
+class s1
+class s2
+
+nominal_datatype lambda: 
+ ('a, 'b) lam =
   Var "name"
-| App "'a lam" "'a lam"
-| Lam x::"name" l::"'a lam"  bind x in l
+| App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
+| Lam x::"name" l::"('a, 'b) lam"  bind x in l
+
+term Var_raw
+term Var
+term App_raw
+term App
+thm Var_def App_def Lam_def
+term abs_lam
+
+thm distinct
+thm lam_raw.inducts
+thm lam_raw.exhaust
+thm fv_defs
+thm bn_defs
+thm perm_simps
+thm perm_laws
+thm lam_raw.size
+thm eq_iff
+thm eq_iff_simps
+thm fv_eqvt
+thm bn_eqvt
+thm size_eqvt
+
+ML {*
+  val qtys = [@{typ "('a::{s1, fs}, 'b::{s2,fs}) lam"}]
+*}
+
+ML {*
+  val thm_a = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct})
+*}
+
+ML {* 
+  val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.induct}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.exhaust}
+*}
+
+ML {*
+  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs}
+*}
 
-ML {* Datatype.read_typ *}
+ML {*
+  val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps}
+*}
+
+ML {*
+  val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws}
+*}
+
+ML {*
+  val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps
+    prod.cases}
+*}
+
+(*  HERE *)
+
+ML {*
+ val thms_e = map (lift_thm @{context} qtys simps)  @{thms eq_iff}
+*}
+
+ML {*
+ val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff_simps}
+*}
+
+
+ML {*
+  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs}
+*}
+
+ML {*
+  val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt}
+*}
+
+ML {*
+  val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt}
+*}
+
+
+
+ML {*
+  space_explode "_raw" "bla_raw2_foo_raw3.0"
+*}
+
 
 
 thm eq_iff