src/FOLP/simpdata.ML
changeset 1463 49ca5e875691
parent 1459 d12da312eff4
child 2603 4988dda71c0b
equal deleted inserted replaced
1462:d991b56cc52a 1463:49ca5e875691
     1 (*  Title:      FOL/simpdata
     1 (*  Title:      FOLP/simpdata.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   1991  University of Cambridge
     4     Copyright   1991  University of Cambridge
     5 
     5 
     6 Simplification data for FOL
     6 Simplification data for FOLP
     7 *)
     7 *)
     8 
     8 
     9 (*** Rewrite rules ***)
     9 (*** Rewrite rules ***)
    10 
    10 
    11 fun int_prove_fun_raw s = 
    11 fun int_prove_fun_raw s =