Hi Denis, > I had the same thought, but I tried: > > lemma > "noBot LNil = True" unfolding noBot_def > using finlsts_rec_LNil > by simp > And it failed. I expected to be able to substitute "using" in Isar > for the "add:" argument to simp. What is different? That is, in general, not the case. Facts chained in to simp (e.g. using "using") are not instantiated wrt. to types, where simp rules given to simp with add: are. Hope this helps Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Attachment:
signature.asc
Description: OpenPGP digital signature