--- a/src/HOL/IOA/Asig.ML Thu Jan 08 18:00:08 1998 +0100
+++ b/src/HOL/IOA/Asig.ML Thu Jan 08 18:00:42 1998 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/IOA/meta_theory/Asig.ML
+(* Title: HOL/IOA/Asig.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
--- a/src/HOL/IOA/Asig.thy Thu Jan 08 18:00:08 1998 +0100
+++ b/src/HOL/IOA/Asig.thy Thu Jan 08 18:00:42 1998 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/IOA/meta_theory/Asig.thy
+(* Title: HOL/IOA/Asig.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
--- a/src/HOL/IOA/IOA.ML Thu Jan 08 18:00:08 1998 +0100
+++ b/src/HOL/IOA/IOA.ML Thu Jan 08 18:00:42 1998 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/IOA/meta_theory/IOA.ML
+(* Title: HOL/IOA/IOA.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
--- a/src/HOL/IOA/IOA.thy Thu Jan 08 18:00:08 1998 +0100
+++ b/src/HOL/IOA/IOA.thy Thu Jan 08 18:00:42 1998 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/IOA/meta_theory/IOA.thy
+(* Title: HOL/IOA/IOA.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
--- a/src/HOL/IOA/Solve.ML Thu Jan 08 18:00:08 1998 +0100
+++ b/src/HOL/IOA/Solve.ML Thu Jan 08 18:00:42 1998 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/IOA/meta_theory/Solve.ML
+(* Title: HOL/IOA/Solve.ML
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
--- a/src/HOL/IOA/Solve.thy Thu Jan 08 18:00:08 1998 +0100
+++ b/src/HOL/IOA/Solve.thy Thu Jan 08 18:00:42 1998 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/IOA/meta_theory/Solve.thy
+(* Title: HOL/IOA/Solve.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen