changeset 13328 | 703de709a64b |
parent 13259 | 01fa0c8dbc92 |
child 13356 | c9cfe1638bf2 |
--- a/src/ZF/ArithSimp.thy Tue Jul 09 23:03:21 2002 +0200 +++ b/src/ZF/ArithSimp.thy Tue Jul 09 23:05:26 2002 +0200 @@ -3,9 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2000 University of Cambridge -Arithmetic with simplification *) +header{*Arithmetic with simplification*} + theory ArithSimp = Arith files "arith_data.ML":