--- 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.
--- 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
*)
--- 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
*)
--- 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
*)
--- 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;
--- 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).
--- 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.
--- 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.
--- 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 *)
--- 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 *)
--- 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$
--- 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.
--- 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.
--- 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.
--- 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.
--- 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.
--- 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.
--- 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.
--- 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
--- 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.