--- a/src/FOL/intprover.ML Mon Jan 29 13:56:41 1996 +0100
+++ b/src/FOL/intprover.ML Mon Jan 29 13:58:15 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/int-prover
+(* Title: FOL/int-prover
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
A naive prover for intuitionistic logic
@@ -56,10 +56,10 @@
(*Attack subgoals using safe inferences -- matching, not resolution*)
val safe_step_tac = FIRST' [eq_assume_tac,
- eq_mp_tac,
- bimatch_tac safe0_brls,
- hyp_subst_tac,
- bimatch_tac safep_brls] ;
+ eq_mp_tac,
+ bimatch_tac safe0_brls,
+ hyp_subst_tac,
+ bimatch_tac safep_brls] ;
(*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;