changeset 1464 | a608f83e3421 |
parent 1459 | d12da312eff4 |
child 5061 | f947332d5465 |
--- a/src/FOLP/ex/prop.ML Tue Jan 30 15:12:53 1996 +0100 +++ b/src/FOLP/ex/prop.ML Tue Jan 30 15:19:20 1996 +0100 @@ -1,4 +1,4 @@ -(* Title: FOL/ex/prop +(* Title: FOLP/ex/prop.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge @@ -7,7 +7,7 @@ Needs declarations of the theory "thy" and the tactic "tac" *) -writeln"File FOL/ex/prop."; +writeln"File FOLP/ex/prop.ML"; writeln"commutative laws of & and | ";