# HG changeset patch # User Christian Urban # Date 1265204208 -3600 # Node ID 68bdd55236083330c485e211ac71892c2952e1af # Parent b1ca92ea3a86e5cdf55339841b3ccbae3ecd4776# Parent c1b469325033f1042f6508148e36414b83d7a4a3 merged diff -r b1ca92ea3a86 -r 68bdd5523608 Quot/Nominal/Terms.thy --- a/Quot/Nominal/Terms.thy Wed Feb 03 14:36:22 2010 +0100 +++ b/Quot/Nominal/Terms.thy Wed Feb 03 14:36:48 2010 +0100 @@ -903,9 +903,9 @@ apply (subst alpha5_INJ) apply (rule_tac x="(x \ y)" in exI) apply (simp only: alpha_gen) -apply (simp add: permute_trm5_lts) -sorry - +apply (simp add: permute_trm5_lts fresh_star_def) +apply (simp add: insert_eqvt eqvts atom_eqvt) +done text {* type schemes *} datatype ty =