# HG changeset patch
# User urbanc
# Date 1133798540 -3600
# Node ID 715d6df89fccd414c12dc79c1397d88d6b0adb26
# Parent  4dd468ccfdf787d0a4ebd6cbe85786f6eac8e537
tuned

diff -r 4dd468ccfdf7 -r 715d6df89fcc src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Mon Dec 05 15:55:19 2005 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Mon Dec 05 17:02:20 2005 +0100
@@ -152,8 +152,8 @@
 using a b c
 apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct)
 apply(auto simp add: sub_def)
-(* FIXME: before using meta-connectives and the new induction *)
-(* method, this was completely automatic *)
+(* FIXME: this was completely automatic before the *)
+(* change to meta-connectives :o(                  *)
 apply(atomize)
 apply(auto)
 done