src/FOLP/intprover.ML
changeset 1459 d12da312eff4
parent 0 a5a9c433f639
child 1463 49ca5e875691
     1.1 --- a/src/FOLP/intprover.ML	Mon Jan 29 13:56:41 1996 +0100
     1.2 +++ b/src/FOLP/intprover.ML	Mon Jan 29 13:58:15 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	FOL/int-prover
     1.5 +(*  Title:      FOL/int-prover
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1992  University of Cambridge
    1.10  
    1.11  A naive prover for intuitionistic logic
    1.12 @@ -54,10 +54,10 @@
    1.13  
    1.14  (*Attack subgoals using safe inferences*)
    1.15  val safe_step_tac = FIRST' [uniq_assume_tac,
    1.16 -			    IFOLP_Lemmas.uniq_mp_tac,
    1.17 -			    biresolve_tac safe0_brls,
    1.18 -			    hyp_subst_tac,
    1.19 -			    biresolve_tac safep_brls] ;
    1.20 +                            IFOLP_Lemmas.uniq_mp_tac,
    1.21 +                            biresolve_tac safe0_brls,
    1.22 +                            hyp_subst_tac,
    1.23 +                            biresolve_tac safep_brls] ;
    1.24  
    1.25  (*Repeatedly attack subgoals using safe inferences*)
    1.26  val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);