changeset 41959 | b460124855b8 |
parent 39685 | d8071cddb877 |
child 44121 | 44adaa6db327 |
--- a/src/HOL/Matrix/Compute_Oracle/linker.ML Sun Mar 13 22:24:10 2011 +0100 +++ b/src/HOL/Matrix/Compute_Oracle/linker.ML Sun Mar 13 22:55:50 2011 +0100 @@ -1,4 +1,4 @@ -(* Title: Tools/Compute_Oracle/linker.ML +(* Title: HOL/Matrix/Compute_Oracle/linker.ML Author: Steven Obua This module solves the problem that the computing oracle does not