diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/Option.ML
--- a/IOA/meta_theory/Option.ML	Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/Option.ML	Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(*  Title:      Option.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1994  TU Muenchen
+
+Derived rules
+*)
+
 val option_rws = Let_def :: Option.option.simps;
 val SS = arith_ss addsimps option_rws;