--- a/src/Tools/induct_tacs.ML Mon Sep 22 08:00:23 2008 +0200 +++ b/src/Tools/induct_tacs.ML Mon Sep 22 08:00:24 2008 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/induct_tacs.ML +(* Title: Tools/induct_tacs.ML ID: $Id$ Author: Makarius