--- 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