tuned
authorurbanc
Sun Dec 04 12:40:39 2005 +0100 (2005-12-04)
changeset 18348b5d7649f8aca
parent 18347 18568b35035a
child 18349 58de95a16d3c
tuned
src/HOL/Nominal/Examples/SN.thy
     1.1 --- a/src/HOL/Nominal/Examples/SN.thy	Sun Dec 04 12:25:57 2005 +0100
     1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Sun Dec 04 12:40:39 2005 +0100
     1.3 @@ -886,5 +886,5 @@
     1.4  (* Abstractions  *)
     1.5  apply(auto dest!: t3_elim simp only: psubst_Lam)
     1.6  apply(rule abs_RED[THEN mp])
     1.7 -apply(force dest: fresh_context simp add: psubs_subs)
     1.8 +apply(force dest: fresh_context simp add: psubst_subst)
     1.9  done
    1.10 \ No newline at end of file