merged
authorwenzelm
Mon, 07 Jun 2010 17:51:26 +0200
changeset 37360 a2cde14de400
parent 37359 7b0ccc20cddc (diff)
parent 37357 b7a55231065a (current diff)
child 37363 ca260a17e013
merged
--- a/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Jun 07 17:50:57 2010 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Jun 07 17:51:26 2010 +0200
@@ -492,7 +492,7 @@
   shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 
 using a b 
 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
-  case (t_VAR \<Gamma>' y T x e' \<Delta>)
+  case (t_VAR y T x e' \<Delta>)
   then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 
        and  a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 
        and  a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
--- a/src/HOL/Nominal/Examples/Nominal_Examples.thy	Mon Jun 07 17:50:57 2010 +0200
+++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy	Mon Jun 07 17:51:26 2010 +0200
@@ -4,23 +4,25 @@
 
 theory Nominal_Examples
 imports
+  CK_Machine
   CR
   CR_Takahashi
   Class3
   Compile
+  Contexts
+  Crary
   Fsub
   Height
   Lambda_mu
+  LocalWeakening
+  Pattern
   SN
-  Weakening
-  Crary
   SOS
-  LocalWeakening
+  Standardization
   Support
-  Contexts
-  Standardization
+  Type_Preservation
   W
-  Pattern
+  Weakening
 begin
 
 end
--- a/src/HOL/Nominal/Examples/Type_Preservation.thy	Mon Jun 07 17:50:57 2010 +0200
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy	Mon Jun 07 17:51:26 2010 +0200
@@ -142,7 +142,7 @@
   shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 
 using a b 
 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
-  case (t_Var \<Gamma>' y T x e' \<Delta>)
+  case (t_Var y T x e' \<Delta>)
   then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 
        and  a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 
        and  a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 07 17:50:57 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Jun 07 17:51:26 2010 +0200
@@ -261,7 +261,7 @@
   end
 
 fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
-                     (relevance_override as {add, del, ...}) ctab =
+                     (relevance_override as {add, del, only}) ctab =
   let
     val thy = ProofContext.theory_of ctxt
     val add_thms = cnf_for_facts ctxt add