src/ZF/ArithSimp.thy
changeset 13328 703de709a64b
parent 13259 01fa0c8dbc92
child 13356 c9cfe1638bf2
equal deleted inserted replaced
13327:be7105a066d3 13328:703de709a64b
     1 (*  Title:      ZF/ArithSimp.ML
     1 (*  Title:      ZF/ArithSimp.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2000  University of Cambridge
     4     Copyright   2000  University of Cambridge
     5 
     5 
     6 Arithmetic with simplification
       
     7 *)
     6 *)
       
     7 
       
     8 header{*Arithmetic with simplification*}
     8 
     9 
     9 theory ArithSimp = Arith
    10 theory ArithSimp = Arith
    10 files "arith_data.ML":
    11 files "arith_data.ML":
    11 
    12 
    12 (*** Difference ***)
    13 (*** Difference ***)