src/FOLP/intprover.ML
changeset 24584 01e83ffa6c54
parent 17496 26535df536ae
child 26322 eaf634e975fa
equal deleted inserted replaced
24583:d77e4d48e497 24584:01e83ffa6c54
     1 (*  Title:      FOLP/int-prover.ML
     1 (*  Title:      FOLP/intprover.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   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 A naive prover for intuitionistic logic
     6 A naive prover for intuitionistic logic