# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1340027402 -3600
# Node ID 1b7c034c9e9ef42a9efe82b9cd3792cf75181c52
# Parent  e46d4ee64221749eecc45375795d88259b7d7d2a
used ML-antiquotation command_spec for new commands

diff -r e46d4ee64221 -r 1b7c034c9e9e Nominal/Ex/Weakening.thy
--- a/Nominal/Ex/Weakening.thy	Tue Jun 12 14:22:58 2012 +0100
+++ b/Nominal/Ex/Weakening.thy	Mon Jun 18 14:50:02 2012 +0100
@@ -49,7 +49,7 @@
 
 nominal_inductive typing
   avoids t_Lam: "x"
-  by (simp_all add: fresh_star_def fresh_ty lam.fresh)
+  by (simp_all add: fresh_star_def fresh_ty)
 
 
 abbreviation
@@ -122,7 +122,7 @@
 
 nominal_inductive typing2
   avoids t2_Lam: "x"
-  by (simp_all add: fresh_star_def fresh_ty lam.fresh)
+  by (simp_all add: fresh_star_def fresh_ty)
 
 lemma weakening_version3: 
   fixes \<Gamma>::"(name \<times> ty) fset"
@@ -133,7 +133,7 @@
 apply(nominal_induct \<Gamma> t T avoiding: x rule: typing2.strong_induct)
 apply(auto)[2]
 apply(rule t2_Lam)
-apply(simp add: fresh_insert_fset fresh_Pair fresh_ty)
+apply(simp add: fresh_insert_fset fresh_ty)
 apply(simp)
 apply(drule_tac x="xa" in meta_spec)
 apply(drule meta_mp)
@@ -147,11 +147,19 @@
   and     b: "(x, T') |\<notin>| \<Gamma>"
   shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T"
 using a b
-apply(induct \<Gamma> t T arbitrary: x)
+apply(induct \<Gamma> t T arbitrary: x T')
 apply(auto)[2]
+apply(blast)
+apply(simp)
+apply(rule_tac ?'a="name" and x="(x, xa, t, T', \<Gamma>)" in obtain_fresh)
+apply(rule_tac t= "Lam [x]. t" and s="Lam [a]. ((a \<leftrightarrow> x) \<bullet> t)" in subst)
+defer
 apply(rule t2_Lam)
+apply(simp add: fresh_insert_fset)
 oops
 
+
+
 end
 
 
diff -r e46d4ee64221 -r 1b7c034c9e9e Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue Jun 12 14:22:58 2012 +0100
+++ b/Nominal/Nominal2.thy	Mon Jun 18 14:50:02 2012 +0100
@@ -748,7 +748,7 @@
 end
 
 (* Command Keyword *)
-val _ = Outer_Syntax.local_theory ("nominal_datatype", Keyword.thy_decl) 
+val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"}
   "declaration of nominal datatypes" 
     (main_parser >> nominal_datatype2_cmd)
 *}
diff -r e46d4ee64221 -r 1b7c034c9e9e Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Tue Jun 12 14:22:58 2012 +0100
+++ b/Nominal/nominal_function.ML	Mon Jun 18 14:50:02 2012 +0100
@@ -274,7 +274,7 @@
 
 (* nominal *)
 val _ =
-  Outer_Syntax.local_theory_to_proof' ("nominal_primrec", Keyword.thy_goal) 
+  Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_primrec"}
     "define general recursive nominal functions"
        (nominal_function_parser nominal_default_config
           >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))
diff -r e46d4ee64221 -r 1b7c034c9e9e Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Tue Jun 12 14:22:58 2012 +0100
+++ b/Nominal/nominal_inductive.ML	Mon Jun 18 14:50:02 2012 +0100
@@ -430,7 +430,7 @@
   val main_parser = Parse.xname -- avoids_parser
 in
   val _ =
-    Outer_Syntax.local_theory_to_proof ("nominal_inductive", Keyword.thy_goal)
+    Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
       "prove strong induction theorem for inductive predicate involving nominal datatypes"
         (main_parser >> prove_strong_inductive_cmd)
 end