# HG changeset patch
# User wenzelm
# Date 1235826598 -3600
# Node ID c26e515f1c29bdca712d809025678424dbf8cbf5
# Parent  5f7b17941730dc97da50ff385b3d7d8352d0b37d
removed Ids;

diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/Compute_Oracle/Compute_Oracle.thy
--- a/src/Tools/Compute_Oracle/Compute_Oracle.thy	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/Compute_Oracle/Compute_Oracle.thy
-    ID:         $Id$
     Author:     Steven Obua, TU Munich
 
 Steven Obua's evaluator.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/Compute_Oracle/am_compiler.ML
--- a/src/Tools/Compute_Oracle/am_compiler.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_compiler.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/Compute_Oracle/am_compiler.ML
-    ID:         $Id$
     Author:     Steven Obua
 *)
 
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/Compute_Oracle/am_ghc.ML
--- a/src/Tools/Compute_Oracle/am_ghc.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_ghc.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/Compute_Oracle/am_ghc.ML
-    ID:         $Id$
     Author:     Steven Obua
 *)
 
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/Compute_Oracle/am_interpreter.ML
--- a/src/Tools/Compute_Oracle/am_interpreter.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_interpreter.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/Compute_Oracle/am_interpreter.ML
-    ID:         $Id$
     Author:     Steven Obua
 *)
 
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/Compute_Oracle/am_sml.ML
--- a/src/Tools/Compute_Oracle/am_sml.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_sml.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/Compute_Oracle/am_sml.ML
-    ID:         $Id$
     Author:     Steven Obua
 
     ToDO: "parameterless rewrite cannot be used in pattern": In a lot of cases it CAN be used, and these cases should be handled properly; 
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/IsaPlanner/README
--- a/src/Tools/IsaPlanner/README	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/IsaPlanner/README	Sat Feb 28 14:09:58 2009 +0100
@@ -1,4 +1,3 @@
-ID:         $Id$
 Author:     Lucas Dixon, University of Edinburgh
 
 Support files for IsaPlanner (see http://isaplanner.sourceforge.net).
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/IsaPlanner/rw_tools.ML
--- a/src/Tools/IsaPlanner/rw_tools.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/IsaPlanner/rw_tools.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/IsaPlanner/rw_tools.ML
-    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
 
 Term related tools used for rewriting.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/IsaPlanner/zipper.ML
--- a/src/Tools/IsaPlanner/zipper.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/IsaPlanner/zipper.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/IsaPlanner/zipper.ML
-    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
 
 A notion roughly based on Huet's Zippers for Isabelle terms.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/Metis/make-metis
--- a/src/Tools/Metis/make-metis	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/Metis/make-metis	Sat Feb 28 14:09:58 2009 +0100
@@ -1,7 +1,5 @@
 #!/usr/bin/env bash
 #
-# $Id$
-#
 # make-metis - turn original Metis files into Isabelle ML source.
 #
 # Structure declarations etc. are made local by wrapping into a
@@ -11,8 +9,6 @@
 THIS=$(cd "$(dirname "$0")"; echo $PWD)
 
 (
-  echo -n '(* $'
-  echo 'Id$ *)'
   cat <<EOF
 (******************************************************************)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/Metis/metis.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,4 +1,3 @@
-(* $Id$ *)
 (******************************************************************)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/README
--- a/src/Tools/README	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/README	Sat Feb 28 14:09:58 2009 +0100
@@ -4,5 +4,3 @@
 This directory contains ML sources of generic tools.  Typically, they
 can be applied to various logics.
 
-
-$Id$
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/atomize_elim.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/atomize_elim.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 Turn elimination rules into atomic expressions in the object logic.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/code/code_haskell.ML
--- a/src/Tools/code/code_haskell.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/code/code_haskell.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/code/code_haskell.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer for Haskell.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/code/code_name.ML
--- a/src/Tools/code/code_name.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/code/code_name.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/code/code_name.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Some code generator infrastructure concerning names.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/code/code_printer.ML
--- a/src/Tools/code/code_printer.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/code/code_printer.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/code/code_printer.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Generic operations for pretty printing of target language code.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/code/code_target.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/code/code_target.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Serializer from intermediate language ("Thin-gol") to target languages.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/float.ML
--- a/src/Tools/float.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/float.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/float.ML
-    ID:         $Id$
     Author:     Steven Obua, Florian Haftmann, TU Muenchen
 
 Implementation of real numbers as mantisse-exponent pairs.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/induct_tacs.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/induct_tacs.ML
-    ID:         $Id$
     Author:     Makarius
 
 Unstructured induction and cases analysis.
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/random_word.ML
--- a/src/Tools/random_word.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/random_word.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/random_word.ML
-    ID:         $Id$
     Author:     Makarius
 
 Simple generator for pseudo-random numbers, using unboxed word
diff -r 5f7b17941730 -r c26e515f1c29 src/Tools/rat.ML
--- a/src/Tools/rat.ML	Sat Feb 28 14:02:12 2009 +0100
+++ b/src/Tools/rat.ML	Sat Feb 28 14:09:58 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Tools/rat.ML
-    ID:         $Id$
     Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
 
 Canonical implementation of exact rational numbers.