expanded tabs
authorclasohm
Mon Jan 29 13:58:15 1996 +0100 (1996-01-29)
changeset 1459d12da312eff4
parent 1458 fd510875fb71
child 1460 5a6f2aabd538
expanded tabs
src/CCL/CCL.ML
src/CCL/Fix.ML
src/CCL/Gfp.ML
src/CCL/Hered.ML
src/CCL/Lfp.ML
src/CCL/Set.ML
src/CCL/Term.ML
src/CCL/Trancl.ML
src/CCL/Type.ML
src/CCL/Wfd.ML
src/CCL/coinduction.ML
src/CCL/equalities.ML
src/CCL/eval.ML
src/CCL/ex/Flag.ML
src/CCL/ex/List.ML
src/CCL/ex/Nat.ML
src/CCL/ex/ROOT.ML
src/CCL/ex/Stream.ML
src/CCL/genrec.ML
src/CCL/mono.ML
src/CCL/subset.ML
src/CCL/typecheck.ML
src/CTT/Arith.ML
src/CTT/Bool.ML
src/CTT/CTT.ML
src/CTT/ROOT.ML
src/CTT/ex/ROOT.ML
src/CTT/ex/equal.ML
src/CTT/ex/synth.ML
src/CTT/ex/typechk.ML
src/CTT/rew.ML
src/Cube/ROOT.ML
src/Cube/ex.ML
src/FOL/FOL.ML
src/FOL/IFOL.ML
src/FOL/ROOT.ML
src/FOL/ex/If.ML
src/FOL/ex/List.ML
src/FOL/ex/Nat.ML
src/FOL/ex/Nat2.ML
src/FOL/ex/NatClass.ML
src/FOL/ex/Prolog.ML
src/FOL/ex/ROOT.ML
src/FOL/ex/cla.ML
src/FOL/ex/foundn.ML
src/FOL/ex/int.ML
src/FOL/ex/intro.ML
src/FOL/ex/mini.ML
src/FOL/ex/prop.ML
src/FOL/ex/quant.ML
src/FOL/intprover.ML
src/FOL/simpdata.ML
src/FOLP/FOLP.ML
src/FOLP/IFOLP.ML
src/FOLP/ROOT.ML
src/FOLP/classical.ML
src/FOLP/ex/If.ML
src/FOLP/ex/Nat.ML
src/FOLP/ex/Prolog.ML
src/FOLP/ex/ROOT.ML
src/FOLP/ex/cla.ML
src/FOLP/ex/foundn.ML
src/FOLP/ex/int.ML
src/FOLP/ex/prop.ML
src/FOLP/ex/quant.ML
src/FOLP/hypsubst.ML
src/FOLP/intprover.ML
src/FOLP/simp.ML
src/FOLP/simpdata.ML
     1.1 --- a/src/CCL/CCL.ML	Mon Jan 29 13:56:41 1996 +0100
     1.2 +++ b/src/CCL/CCL.ML	Mon Jan 29 13:58:15 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	CCL/ccl
     1.5 +(*  Title:      CCL/ccl
     1.6      ID:         $Id$
     1.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  For ccl.thy.
    1.12 @@ -89,7 +89,7 @@
    1.13           | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
    1.14             val sg = sign_of thy;
    1.15             val T = case Sign.const_type sg sy of
    1.16 -  		            None => error(sy^" not declared") | Some(T) => T;
    1.17 +                            None => error(sy^" not declared") | Some(T) => T;
    1.18             val arity = length (fst (strip_type T));
    1.19         in sy ^ (arg_str arity name "") end;
    1.20  
     2.1 --- a/src/CCL/Fix.ML	Mon Jan 29 13:56:41 1996 +0100
     2.2 +++ b/src/CCL/Fix.ML	Mon Jan 29 13:58:15 1996 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4 -(*  Title: 	CCL/fix
     2.5 +(*  Title:      CCL/fix
     2.6      ID:         $Id$
     2.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
     2.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     2.9      Copyright   1993  University of Cambridge
    2.10  
    2.11  For fix.thy.
     3.1 --- a/src/CCL/Gfp.ML	Mon Jan 29 13:56:41 1996 +0100
     3.2 +++ b/src/CCL/Gfp.ML	Mon Jan 29 13:58:15 1996 +0100
     3.3 @@ -1,9 +1,9 @@
     3.4 -(*  Title: 	CCL/gfp
     3.5 +(*  Title:      CCL/gfp
     3.6      ID:         $Id$
     3.7  
     3.8  Modified version of
     3.9 -    Title: 	HOL/gfp
    3.10 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    3.11 +    Title:      HOL/gfp
    3.12 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    3.13      Copyright   1993  University of Cambridge
    3.14  
    3.15  For gfp.thy.  The Knaster-Tarski Theorem for greatest fixed points.
    3.16 @@ -28,12 +28,12 @@
    3.17  
    3.18  val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) <= f(gfp(f))";
    3.19  by (EVERY1 [rtac gfp_least, rtac subset_trans, atac,
    3.20 -	    rtac (mono RS monoD), rtac gfp_upperbound, atac]);
    3.21 +            rtac (mono RS monoD), rtac gfp_upperbound, atac]);
    3.22  qed "gfp_lemma2";
    3.23  
    3.24  val [mono] = goal Gfp.thy "mono(f) ==> f(gfp(f)) <= gfp(f)";
    3.25  by (EVERY1 [rtac gfp_upperbound, rtac (mono RS monoD), 
    3.26 -	    rtac gfp_lemma2, rtac mono]);
    3.27 +            rtac gfp_lemma2, rtac mono]);
    3.28  qed "gfp_lemma3";
    3.29  
    3.30  val [mono] = goal Gfp.thy "mono(f) ==> gfp(f) = f(gfp(f))";
     4.1 --- a/src/CCL/Hered.ML	Mon Jan 29 13:56:41 1996 +0100
     4.2 +++ b/src/CCL/Hered.ML	Mon Jan 29 13:58:15 1996 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4 -(*  Title: 	CCL/hered
     4.5 +(*  Title:      CCL/hered
     4.6      ID:         $Id$
     4.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
     4.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     4.9      Copyright   1993  University of Cambridge
    4.10  
    4.11  For hered.thy.
     5.1 --- a/src/CCL/Lfp.ML	Mon Jan 29 13:56:41 1996 +0100
     5.2 +++ b/src/CCL/Lfp.ML	Mon Jan 29 13:58:15 1996 +0100
     5.3 @@ -1,9 +1,9 @@
     5.4 -(*  Title: 	CCL/lfp
     5.5 +(*  Title:      CCL/lfp
     5.6      ID:         $Id$
     5.7  
     5.8  Modified version of
     5.9 -    Title: 	HOL/lfp.ML
    5.10 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    5.11 +    Title:      HOL/lfp.ML
    5.12 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    5.13      Copyright   1992  University of Cambridge
    5.14  
    5.15  For lfp.thy.  The Knaster-Tarski Theorem
    5.16 @@ -28,12 +28,12 @@
    5.17  
    5.18  val [mono] = goal Lfp.thy "mono(f) ==> f(lfp(f)) <= lfp(f)";
    5.19  by (EVERY1 [rtac lfp_greatest, rtac subset_trans,
    5.20 -	    rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
    5.21 +            rtac (mono RS monoD), rtac lfp_lowerbound, atac, atac]);
    5.22  qed "lfp_lemma2";
    5.23  
    5.24  val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) <= f(lfp(f))";
    5.25  by (EVERY1 [rtac lfp_lowerbound, rtac (mono RS monoD), 
    5.26 -	    rtac lfp_lemma2, rtac mono]);
    5.27 +            rtac lfp_lemma2, rtac mono]);
    5.28  qed "lfp_lemma3";
    5.29  
    5.30  val [mono] = goal Lfp.thy "mono(f) ==> lfp(f) = f(lfp(f))";
    5.31 @@ -44,15 +44,15 @@
    5.32  (*** General induction rule for least fixed points ***)
    5.33  
    5.34  val [lfp,mono,indhyp] = goal Lfp.thy
    5.35 -    "[| a: lfp(f);  mono(f);  				\
    5.36 -\       !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x) 	\
    5.37 +    "[| a: lfp(f);  mono(f);                            \
    5.38 +\       !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x)   \
    5.39  \    |] ==> P(a)";
    5.40  by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);
    5.41  by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
    5.42  by (EVERY1 [rtac Int_greatest, rtac subset_trans, 
    5.43 -	    rtac (Int_lower1 RS (mono RS monoD)),
    5.44 -	    rtac (mono RS lfp_lemma2),
    5.45 -	    rtac (CollectI RS subsetI), rtac indhyp, atac]);
    5.46 +            rtac (Int_lower1 RS (mono RS monoD)),
    5.47 +            rtac (mono RS lfp_lemma2),
    5.48 +            rtac (CollectI RS subsetI), rtac indhyp, atac]);
    5.49  qed "induct";
    5.50  
    5.51  (** Definition forms of lfp_Tarski and induct, to control unfolding **)
    5.52 @@ -63,11 +63,11 @@
    5.53  qed "def_lfp_Tarski";
    5.54  
    5.55  val rew::prems = goal Lfp.thy
    5.56 -    "[| A == lfp(f);  a:A;  mono(f);   			\
    5.57 -\       !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x) 	\
    5.58 +    "[| A == lfp(f);  a:A;  mono(f);                    \
    5.59 +\       !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x)        \
    5.60  \    |] ==> P(a)";
    5.61 -by (EVERY1 [rtac induct,	(*backtracking to force correct induction*)
    5.62 -	    REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
    5.63 +by (EVERY1 [rtac induct,        (*backtracking to force correct induction*)
    5.64 +            REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
    5.65  qed "def_induct";
    5.66  
    5.67  (*Monotonicity of lfp!*)
     6.1 --- a/src/CCL/Set.ML	Mon Jan 29 13:56:41 1996 +0100
     6.2 +++ b/src/CCL/Set.ML	Mon Jan 29 13:58:15 1996 +0100
     6.3 @@ -1,11 +1,11 @@
     6.4 -(*  Title: 	set/set
     6.5 +(*  Title:      set/set
     6.6      ID:         $Id$
     6.7  
     6.8  For set.thy.
     6.9  
    6.10  Modified version of
    6.11 -    Title: 	HOL/set
    6.12 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    6.13 +    Title:      HOL/set
    6.14 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    6.15      Copyright   1991  University of Cambridge
    6.16  
    6.17  For set.thy.  Set theory for higher-order logic.  A set is simply a predicate.
    6.18 @@ -282,7 +282,7 @@
    6.19  \    (UN x:A. C(x)) = (UN x:B. D(x))";
    6.20  by (REPEAT (etac UN_E 1
    6.21       ORELSE ares_tac ([UN_I,equalityI,subsetI] @ 
    6.22 -		      (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
    6.23 +                      (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
    6.24  qed "UN_cong";
    6.25  
    6.26  (*** Intersections of families -- INTER x:A. B(x) is Inter(B)``A ) *)
     7.1 --- a/src/CCL/Term.ML	Mon Jan 29 13:56:41 1996 +0100
     7.2 +++ b/src/CCL/Term.ML	Mon Jan 29 13:58:15 1996 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4 -(*  Title: 	CCL/terms
     7.5 +(*  Title:      CCL/terms
     7.6      ID:         $Id$
     7.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
     7.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     7.9      Copyright   1993  University of Cambridge
    7.10  
    7.11  For terms.thy.
    7.12 @@ -57,12 +57,12 @@
    7.13  
    7.14  fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
    7.15             (fn _ => [rtac (letrecB RS ssubst) 1,
    7.16 -		     simp_tac (CCL_ss addsimps rawBs) 1]);
    7.17 +                     simp_tac (CCL_ss addsimps rawBs) 1]);
    7.18  fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    7.19  
    7.20  fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s
    7.21             (fn _ => [simp_tac (CCL_ss addsimps rawBs 
    7.22 -			       setloop (rtac (letrecB RS ssubst))) 1]);
    7.23 +                               setloop (rtac (letrecB RS ssubst))) 1]);
    7.24  fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
    7.25  
    7.26  val ifBtrue    = mk_beta_rl "if true then t else u = t";
    7.27 @@ -116,7 +116,7 @@
    7.28  (*** Constructors are injective ***)
    7.29  
    7.30  val term_injs = map (mk_inj_rl Term.thy 
    7.31 -		     [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons])
    7.32 +                     [applyB,splitB,whenBinl,whenBinr,ncaseBsucc,lcaseBcons])
    7.33                 ["(inl(a) = inl(a')) <-> (a=a')",
    7.34                  "(inr(a) = inr(a')) <-> (a=a')",
    7.35                  "(succ(a) = succ(a')) <-> (a=a')",
     8.1 --- a/src/CCL/Trancl.ML	Mon Jan 29 13:56:41 1996 +0100
     8.2 +++ b/src/CCL/Trancl.ML	Mon Jan 29 13:58:15 1996 +0100
     8.3 @@ -1,11 +1,11 @@
     8.4 -(*  Title: 	CCL/trancl
     8.5 +(*  Title:      CCL/trancl
     8.6      ID:         $Id$
     8.7  
     8.8  For trancl.thy.
     8.9  
    8.10  Modified version of
    8.11 -    Title: 	HOL/trancl.ML
    8.12 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    8.13 +    Title:      HOL/trancl.ML
    8.14 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    8.15      Copyright   1992  University of Cambridge
    8.16  
    8.17  *)
    8.18 @@ -66,8 +66,8 @@
    8.19  qed "compEpair";
    8.20  
    8.21  val comp_cs = set_cs addIs [compI,idI] 
    8.22 -		       addEs [compE,idE] 
    8.23 -		       addSEs [pair_inject];
    8.24 +                       addEs [compE,idE] 
    8.25 +                       addSEs [pair_inject];
    8.26  
    8.27  val prems = goal Trancl.thy
    8.28      "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    8.29 @@ -120,7 +120,7 @@
    8.30  val major::prems = goal Trancl.thy
    8.31      "[| <a,b> : r^*;    \
    8.32  \       P(a); \
    8.33 -\	!!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z) |]  \
    8.34 +\       !!y z.[| <a,y> : r^*;  <y,z> : r;  P(y) |] ==> P(z) |]  \
    8.35  \     ==> P(b)";
    8.36  (*by induction on this formula*)
    8.37  by (subgoal_tac "ALL y. <a,b> = <a,y> --> P(y)" 1);
    8.38 @@ -142,7 +142,7 @@
    8.39  (*elimination of rtrancl -- by induction on a special formula*)
    8.40  val major::prems = goal Trancl.thy
    8.41      "[| <a,b> : r^*;  (a = b) ==> P; \
    8.42 -\	!!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \
    8.43 +\       !!y.[| <a,y> : r^*; <y,b> : r |] ==> P |] \
    8.44  \    ==> P";
    8.45  by (subgoal_tac "a = b  | (EX y. <a,y> : r^* & <y,b> : r)" 1);
    8.46  by (rtac (major RS rtrancl_induct) 2);
    8.47 @@ -188,7 +188,7 @@
    8.48  val major::prems = goal Trancl.thy
    8.49      "[| <a,b> : r^+;  \
    8.50  \       <a,b> : r ==> P; \
    8.51 -\	!!y.[| <a,y> : r^+;  <y,b> : r |] ==> P  \
    8.52 +\       !!y.[| <a,y> : r^+;  <y,b> : r |] ==> P  \
    8.53  \    |] ==> P";
    8.54  by (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+  &  <y,b> : r)" 1);
    8.55  by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
     9.1 --- a/src/CCL/Type.ML	Mon Jan 29 13:56:41 1996 +0100
     9.2 +++ b/src/CCL/Type.ML	Mon Jan 29 13:58:15 1996 +0100
     9.3 @@ -1,6 +1,6 @@
     9.4 -(*  Title: 	CCL/types
     9.5 +(*  Title:      CCL/types
     9.6      ID:         $Id$
     9.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
     9.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
     9.9      Copyright   1992  University of Cambridge
    9.10  
    9.11  For types.thy.
    10.1 --- a/src/CCL/Wfd.ML	Mon Jan 29 13:56:41 1996 +0100
    10.2 +++ b/src/CCL/Wfd.ML	Mon Jan 29 13:58:15 1996 +0100
    10.3 @@ -1,11 +1,11 @@
    10.4 -(*  Title: 	CCL/wfd.ML
    10.5 +(*  Title:      CCL/wfd.ML
    10.6      ID:         $Id$
    10.7  
    10.8  For wfd.thy.
    10.9  
   10.10  Based on
   10.11 -    Titles: 	ZF/wf.ML and HOL/ex/lex-prod
   10.12 -    Authors: 	Lawrence C Paulson and Tobias Nipkow
   10.13 +    Titles:     ZF/wf.ML and HOL/ex/lex-prod
   10.14 +    Authors:    Lawrence C Paulson and Tobias Nipkow
   10.15      Copyright   1992  University of Cambridge
   10.16  
   10.17  *)
    11.1 --- a/src/CCL/coinduction.ML	Mon Jan 29 13:56:41 1996 +0100
    11.2 +++ b/src/CCL/coinduction.ML	Mon Jan 29 13:58:15 1996 +0100
    11.3 @@ -1,6 +1,6 @@
    11.4 -(*  Title: 	92/CCL/coinduction
    11.5 +(*  Title:      92/CCL/coinduction
    11.6      ID:         $Id$
    11.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    11.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    11.9      Copyright   1993  University of Cambridge
   11.10  
   11.11  Lemmas and tactics for using the rule coinduct3 on [= and =.
    12.1 --- a/src/CCL/equalities.ML	Mon Jan 29 13:56:41 1996 +0100
    12.2 +++ b/src/CCL/equalities.ML	Mon Jan 29 13:58:15 1996 +0100
    12.3 @@ -1,9 +1,9 @@
    12.4 -(*  Title: 	CCL/equalities
    12.5 +(*  Title:      CCL/equalities
    12.6      ID:         $Id$
    12.7  
    12.8  Modified version of
    12.9 -    Title: 	HOL/equalities
   12.10 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
   12.11 +    Title:      HOL/equalities
   12.12 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   12.13      Copyright   1991  University of Cambridge
   12.14  
   12.15  Equalities involving union, intersection, inclusion, etc.
    13.1 --- a/src/CCL/eval.ML	Mon Jan 29 13:56:41 1996 +0100
    13.2 +++ b/src/CCL/eval.ML	Mon Jan 29 13:58:15 1996 +0100
    13.3 @@ -1,6 +1,6 @@
    13.4 -(*  Title: 	92/CCL/eval
    13.5 +(*  Title:      92/CCL/eval
    13.6      ID:         $Id$
    13.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    13.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    13.9      Copyright   1992  University of Cambridge
   13.10  
   13.11  *)
    14.1 --- a/src/CCL/ex/Flag.ML	Mon Jan 29 13:56:41 1996 +0100
    14.2 +++ b/src/CCL/ex/Flag.ML	Mon Jan 29 13:58:15 1996 +0100
    14.3 @@ -1,6 +1,6 @@
    14.4 -(*  Title: 	CCL/ex/flag
    14.5 +(*  Title:      CCL/ex/flag
    14.6      ID:         $Id$
    14.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    14.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    14.9      Copyright   1993  University of Cambridge
   14.10  
   14.11  For flag.thy.
   14.12 @@ -35,8 +35,8 @@
   14.13      "flag : List(Colour)->List(Colour)*List(Colour)*List(Colour)";
   14.14  by (typechk_tac [redT,whiteT,blueT,ccaseT] 1);
   14.15  by clean_ccs_tac;
   14.16 -be (ListPRI RS (ListPR_wf RS wfI)) 1;
   14.17 -ba 1;
   14.18 +by (etac (ListPRI RS (ListPR_wf RS wfI)) 1);
   14.19 +by (assume_tac 1);
   14.20  result();
   14.21  
   14.22  
    15.1 --- a/src/CCL/ex/List.ML	Mon Jan 29 13:56:41 1996 +0100
    15.2 +++ b/src/CCL/ex/List.ML	Mon Jan 29 13:58:15 1996 +0100
    15.3 @@ -1,6 +1,6 @@
    15.4 -(*  Title: 	CCL/ex/list
    15.5 +(*  Title:      CCL/ex/list
    15.6      ID:         $Id$
    15.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    15.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    15.9      Copyright   1993  University of Cambridge
   15.10  
   15.11  For list.thy.
   15.12 @@ -32,12 +32,12 @@
   15.13  (****)
   15.14  
   15.15  val [prem] = goal List.thy "n:Nat ==> map(f) ^ n ` [] = []";
   15.16 -br (prem RS Nat_ind) 1;
   15.17 +by (rtac (prem RS Nat_ind) 1);
   15.18  by (ALLGOALS (asm_simp_tac list_ss));
   15.19  qed "nmapBnil";
   15.20  
   15.21  val [prem] = goal List.thy "n:Nat ==> map(f)^n`(x$xs) = (f^n`x)$(map(f)^n`xs)";
   15.22 -br (prem RS Nat_ind) 1;
   15.23 +by (rtac (prem RS Nat_ind) 1);
   15.24  by (ALLGOALS (asm_simp_tac list_ss));
   15.25  qed "nmapBcons";
   15.26  
   15.27 @@ -85,8 +85,8 @@
   15.28    "[| f:A->Bool;  l : List(A) |] ==> partition(f,l) : List(A)*List(A)";
   15.29  by (typechk_tac prems 1);
   15.30  by clean_ccs_tac;
   15.31 -br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2;
   15.32 -br (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1;
   15.33 +by (rtac (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 2);
   15.34 +by (rtac (ListPRI RS wfstI RS (ListPR_wf RS wmap_wf RS wfI)) 1);
   15.35  by (REPEAT (atac 1));
   15.36  qed "partitionT";
   15.37  
    16.1 --- a/src/CCL/ex/Nat.ML	Mon Jan 29 13:56:41 1996 +0100
    16.2 +++ b/src/CCL/ex/Nat.ML	Mon Jan 29 13:58:15 1996 +0100
    16.3 @@ -1,6 +1,6 @@
    16.4 -(*  Title: 	CCL/ex/nat
    16.5 +(*  Title:      CCL/ex/nat
    16.6      ID:         $Id$
    16.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    16.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    16.9      Copyright   1993  University of Cambridge
   16.10  
   16.11  For nat.thy.
   16.12 @@ -25,7 +25,7 @@
   16.13  (*** Lemma for napply ***)
   16.14  
   16.15  val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a";
   16.16 -br (prem RS Nat_ind) 1;
   16.17 +by (rtac (prem RS Nat_ind) 1);
   16.18  by (ALLGOALS (asm_simp_tac nat_ss));
   16.19  qed "napply_f";
   16.20  
   16.21 @@ -43,13 +43,13 @@
   16.22  val prems = goalw Nat.thy [sub_def] "[| a:Nat;  b:Nat |] ==> a #- b : Nat";
   16.23  by (typechk_tac (prems) 1);
   16.24  by clean_ccs_tac;
   16.25 -be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
   16.26 +by (etac (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1);
   16.27  qed "subT";
   16.28  
   16.29  val prems = goalw Nat.thy [le_def] "[| a:Nat;  b:Nat |] ==> a #<= b : Bool";
   16.30  by (typechk_tac (prems) 1);
   16.31  by clean_ccs_tac;
   16.32 -be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
   16.33 +by (etac (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1);
   16.34  qed "leT";
   16.35  
   16.36  val prems = goalw Nat.thy [not_def,lt_def] "[| a:Nat;  b:Nat |] ==> a #< b : Bool";
    17.1 --- a/src/CCL/ex/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
    17.2 +++ b/src/CCL/ex/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
    17.3 @@ -6,7 +6,7 @@
    17.4  Executes all examples for Classical Computational Logic
    17.5  *)
    17.6  
    17.7 -CCL_build_completed;	(*Cause examples to fail if CCL did*)
    17.8 +CCL_build_completed;    (*Cause examples to fail if CCL did*)
    17.9  
   17.10  writeln"Root file for CCL examples";
   17.11  proof_timing := true;
    18.1 --- a/src/CCL/ex/Stream.ML	Mon Jan 29 13:56:41 1996 +0100
    18.2 +++ b/src/CCL/ex/Stream.ML	Mon Jan 29 13:58:15 1996 +0100
    18.3 @@ -1,6 +1,6 @@
    18.4 -(*  Title: 	CCL/ex/stream
    18.5 +(*  Title:      CCL/ex/stream
    18.6      ID:         $Id$
    18.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    18.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    18.9      Copyright   1993  University of Cambridge
   18.10  
   18.11  For stream.thy.
   18.12 @@ -19,7 +19,7 @@
   18.13         "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}"  1);
   18.14  by (fast_tac (ccl_cs addSIs prems) 1);
   18.15  by (safe_tac type_cs);
   18.16 -be (XH_to_E ListsXH) 1;
   18.17 +by (etac (XH_to_E ListsXH) 1);
   18.18  by (EQgen_tac list_ss [] 1);
   18.19  by (simp_tac list_ss 1);
   18.20  by (fast_tac ccl_cs 1);
   18.21 @@ -32,7 +32,7 @@
   18.22         "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(%x.x,l) & y=l)}"  1);
   18.23  by (fast_tac (ccl_cs addSIs prems) 1);
   18.24  by (safe_tac type_cs);
   18.25 -be (XH_to_E ListsXH) 1;
   18.26 +by (etac (XH_to_E ListsXH) 1);
   18.27  by (EQgen_tac list_ss [] 1);
   18.28  by (fast_tac ccl_cs 1);
   18.29  qed "map_id";
   18.30 @@ -45,9 +45,9 @@
   18.31  \                                           x=map(f,l@m) & y=map(f,l) @ map(f,m))}"  1);
   18.32  by (fast_tac (ccl_cs addSIs prems) 1);
   18.33  by (safe_tac type_cs);
   18.34 -be (XH_to_E ListsXH) 1;
   18.35 +by (etac (XH_to_E ListsXH) 1);
   18.36  by (EQgen_tac list_ss [] 1);
   18.37 -be (XH_to_E ListsXH) 1;
   18.38 +by (etac (XH_to_E ListsXH) 1);
   18.39  by (EQgen_tac list_ss [] 1);
   18.40  by (fast_tac ccl_cs 1);
   18.41  qed "map_append";
   18.42 @@ -61,7 +61,7 @@
   18.43  \                          x=k @ l @ m & y=(k @ l) @ m)}"  1);
   18.44  by (fast_tac (ccl_cs addSIs prems) 1);
   18.45  by (safe_tac type_cs);
   18.46 -be (XH_to_E ListsXH) 1;
   18.47 +by (etac (XH_to_E ListsXH) 1);
   18.48  by (EQgen_tac list_ss [] 1);
   18.49  by (fast_tac ccl_cs 2);
   18.50  by (DEPTH_SOLVE (etac (XH_to_E ListsXH) 1 THEN EQgen_tac list_ss [] 1));
   18.51 @@ -74,7 +74,7 @@
   18.52      "{p. EX x y.p=<x,y> & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1);
   18.53  by (fast_tac (ccl_cs addSIs prems) 1);
   18.54  by (safe_tac set_cs);
   18.55 -be (XH_to_E IListsXH) 1;
   18.56 +by (etac (XH_to_E IListsXH) 1);
   18.57  by (EQgen_tac list_ss [] 1);
   18.58  by (fast_tac ccl_cs 1);
   18.59  qed "ilist_append";
   18.60 @@ -85,13 +85,13 @@
   18.61  (*        fun iter2(f,a) = a$map(f,iter2(f,a))                        *)
   18.62  
   18.63  goalw Stream.thy [iter1_def] "iter1(f,a) = a$iter1(f,f(a))";
   18.64 -br (letrecB RS trans) 1;
   18.65 +by (rtac (letrecB RS trans) 1);
   18.66  by (simp_tac term_ss 1);
   18.67  qed "iter1B";
   18.68  
   18.69  goalw Stream.thy [iter2_def] "iter2(f,a) = a $ map(f,iter2(f,a))";
   18.70 -br (letrecB RS trans) 1;
   18.71 -br refl 1;
   18.72 +by (rtac (letrecB RS trans) 1);
   18.73 +by (rtac refl 1);
   18.74  qed "iter2B";
   18.75  
   18.76  val [prem] =goal Stream.thy
   18.77 @@ -106,7 +106,7 @@
   18.78      "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
   18.79      1);
   18.80  by (fast_tac (type_cs addSIs [napplyBzero RS sym,
   18.81 -			      napplyBzero RS sym RS arg_cong]) 1);
   18.82 +                              napplyBzero RS sym RS arg_cong]) 1);
   18.83  by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
   18.84  by (rtac (napply_f RS ssubst) 1 THEN atac 1);
   18.85  by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
    19.1 --- a/src/CCL/genrec.ML	Mon Jan 29 13:56:41 1996 +0100
    19.2 +++ b/src/CCL/genrec.ML	Mon Jan 29 13:58:15 1996 +0100
    19.3 @@ -1,6 +1,6 @@
    19.4 -(*  Title: 	92/CCL/genrec
    19.5 +(*  Title:      92/CCL/genrec
    19.6      ID:         $Id$
    19.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    19.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    19.9      Copyright   1993  University of Cambridge
   19.10  
   19.11  *)
    20.1 --- a/src/CCL/mono.ML	Mon Jan 29 13:56:41 1996 +0100
    20.2 +++ b/src/CCL/mono.ML	Mon Jan 29 13:58:15 1996 +0100
    20.3 @@ -1,9 +1,9 @@
    20.4 -(*  Title: 	CCL/mono
    20.5 +(*  Title:      CCL/mono
    20.6      ID:         $Id$
    20.7  
    20.8  Modified version of
    20.9 -    Title: 	HOL/mono
   20.10 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
   20.11 +    Title:      HOL/mono
   20.12 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   20.13      Copyright   1991  University of Cambridge
   20.14  
   20.15  Monotonicity of various operations
    21.1 --- a/src/CCL/subset.ML	Mon Jan 29 13:56:41 1996 +0100
    21.2 +++ b/src/CCL/subset.ML	Mon Jan 29 13:58:15 1996 +0100
    21.3 @@ -1,9 +1,9 @@
    21.4 -(*  Title: 	CCL/subset
    21.5 +(*  Title:      CCL/subset
    21.6      ID:         $Id$
    21.7  
    21.8  Modified version of
    21.9 -    Title: 	HOL/subset
   21.10 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
   21.11 +    Title:      HOL/subset
   21.12 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   21.13      Copyright   1991  University of Cambridge
   21.14  
   21.15  Derived rules involving subsets
   21.16 @@ -99,10 +99,10 @@
   21.17  
   21.18  val set_cs = FOL_cs 
   21.19      addSIs [ballI, subsetI, InterI, INT_I, CollectI, 
   21.20 -	    ComplI, IntI, UnCI, singletonI] 
   21.21 +            ComplI, IntI, UnCI, singletonI] 
   21.22      addIs  [bexI, UnionI, UN_I] 
   21.23      addSEs [bexE, UnionE, UN_E,
   21.24 -	    CollectE, ComplE, IntE, UnE, emptyE, singletonE] 
   21.25 +            CollectE, ComplE, IntE, UnE, emptyE, singletonE] 
   21.26      addEs  [ballE, InterD, InterE, INT_D, INT_E, subsetD, subsetCE];
   21.27  
   21.28  fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
    22.1 --- a/src/CCL/typecheck.ML	Mon Jan 29 13:56:41 1996 +0100
    22.2 +++ b/src/CCL/typecheck.ML	Mon Jan 29 13:58:15 1996 +0100
    22.3 @@ -1,6 +1,6 @@
    22.4 -(*  Title: 	CCL/typecheck
    22.5 +(*  Title:      CCL/typecheck
    22.6      ID:         $Id$
    22.7 -    Author: 	Martin Coen, Cambridge University Computer Laboratory
    22.8 +    Author:     Martin Coen, Cambridge University Computer Laboratory
    22.9      Copyright   1993  University of Cambridge
   22.10  
   22.11  *)
    23.1 --- a/src/CTT/Arith.ML	Mon Jan 29 13:56:41 1996 +0100
    23.2 +++ b/src/CTT/Arith.ML	Mon Jan 29 13:58:15 1996 +0100
    23.3 @@ -1,6 +1,6 @@
    23.4 -(*  Title: 	CTT/arith
    23.5 +(*  Title:      CTT/arith
    23.6      ID:         $Id$
    23.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    23.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.9      Copyright   1991  University of Cambridge
   23.10  
   23.11  Theorems for arith.thy (Arithmetic operators)
   23.12 @@ -120,14 +120,14 @@
   23.13  
   23.14  structure Arith_simp_data: TSIMP_DATA =
   23.15    struct
   23.16 -  val refl		= refl_elem
   23.17 -  val sym		= sym_elem
   23.18 -  val trans		= trans_elem
   23.19 -  val refl_red		= refl_red
   23.20 -  val trans_red		= trans_red
   23.21 -  val red_if_equal	= red_if_equal
   23.22 -  val default_rls 	= arithC_rls @ comp_rls
   23.23 -  val routine_tac 	= routine_tac (arith_typing_rls @ routine_rls)
   23.24 +  val refl              = refl_elem
   23.25 +  val sym               = sym_elem
   23.26 +  val trans             = trans_elem
   23.27 +  val refl_red          = refl_red
   23.28 +  val trans_red         = trans_red
   23.29 +  val red_if_equal      = red_if_equal
   23.30 +  val default_rls       = arithC_rls @ comp_rls
   23.31 +  val routine_tac       = routine_tac (arith_typing_rls @ routine_rls)
   23.32    end;
   23.33  
   23.34  structure Arith_simp = TSimpFun (Arith_simp_data);
   23.35 @@ -159,7 +159,7 @@
   23.36    [ (NE_tac "a" 1),
   23.37      (hyp_arith_rew_tac prems),
   23.38      (NE_tac "b" 2),
   23.39 -    (resolve_tac [sym_elem] 1),
   23.40 +    (rtac sym_elem 1),
   23.41      (NE_tac "b" 1),
   23.42      (hyp_arith_rew_tac prems) ]);
   23.43  
   23.44 @@ -175,7 +175,7 @@
   23.45    [ (NE_tac "a" 1),
   23.46      (hyp_arith_rew_tac prems),
   23.47      (NE_tac "b" 2),
   23.48 -    (resolve_tac [sym_elem] 1),
   23.49 +    (rtac sym_elem 1),
   23.50      (NE_tac "b" 1),
   23.51      (hyp_arith_rew_tac prems) ]);   NEEDS COMMUTATIVE MATCHING
   23.52  ***************)
   23.53 @@ -198,7 +198,7 @@
   23.54      (REPEAT (assume_tac 1  ORELSE  
   23.55              resolve_tac
   23.56               (prems@[add_commute,mult_typingL,add_typingL]@
   23.57 -	       intrL_rls@[refl_elem])   1)) ]);
   23.58 +               intrL_rls@[refl_elem])   1)) ]);
   23.59  
   23.60  (*Commutative law for multiplication*)
   23.61  qed_goal "mult_commute" Arith.thy 
   23.62 @@ -254,8 +254,8 @@
   23.63      (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
   23.64  by (NE_tac "x" 4 THEN assume_tac 4); 
   23.65  (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
   23.66 -by (resolve_tac [replace_type] 5);
   23.67 -by (resolve_tac [replace_type] 4);
   23.68 +by (rtac replace_type 5);
   23.69 +by (rtac replace_type 4);
   23.70  by (arith_rew_tac prems); 
   23.71  (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   23.72    Both follow by rewriting, (2) using quantified induction hyp*)
   23.73 @@ -271,7 +271,7 @@
   23.74      the use of RS below instantiates Vars in ProdE automatically. *)
   23.75  val prems =
   23.76  goal Arith.thy "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N";
   23.77 -by (resolve_tac [EqE] 1);
   23.78 +by (rtac EqE 1);
   23.79  by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
   23.80  by (REPEAT (resolve_tac (prems@[EqI]) 1));
   23.81  qed "add_diff_inverse";
   23.82 @@ -310,7 +310,7 @@
   23.83  (*Note how easy using commutative laws can be?  ...not always... *)
   23.84  val prems = goalw Arith.thy [absdiff_def]
   23.85      "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
   23.86 -by (resolve_tac [add_commute] 1);
   23.87 +by (rtac add_commute 1);
   23.88  by (typechk_tac ([diff_typing]@prems));
   23.89  qed "absdiff_commute";
   23.90  
   23.91 @@ -318,7 +318,7 @@
   23.92  val prems =
   23.93  goal Arith.thy "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)";
   23.94  by (NE_tac "a" 1);
   23.95 -by (resolve_tac [replace_type] 3);
   23.96 +by (rtac replace_type 3);
   23.97  by (arith_rew_tac prems);
   23.98  by (intr_tac[]);  (*strips remaining PRODs*)
   23.99  by (resolve_tac [ zero_ne_succ RS FE ] 2);
  23.100 @@ -330,9 +330,9 @@
  23.101    Again, resolution instantiates variables in ProdE *)
  23.102  val prems =
  23.103  goal Arith.thy "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N";
  23.104 -by (resolve_tac [EqE] 1);
  23.105 +by (rtac EqE 1);
  23.106  by (resolve_tac [add_eq0_lemma RS ProdE] 1);
  23.107 -by (resolve_tac [EqI] 3);
  23.108 +by (rtac EqI 3);
  23.109  by (ALLGOALS (resolve_tac prems));
  23.110  qed "add_eq0";
  23.111  
  23.112 @@ -342,8 +342,8 @@
  23.113  \    ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)";
  23.114  by (intr_tac[]);
  23.115  by eqintr_tac;
  23.116 -by (resolve_tac [add_eq0] 2);
  23.117 -by (resolve_tac [add_eq0] 1);
  23.118 +by (rtac add_eq0 2);
  23.119 +by (rtac add_eq0 1);
  23.120  by (resolve_tac [add_commute RS trans_elem] 6);
  23.121  by (typechk_tac (diff_typing::prems));
  23.122  qed "absdiff_eq0_lem";
  23.123 @@ -352,12 +352,12 @@
  23.124    proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
  23.125  val prems =
  23.126  goal Arith.thy "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
  23.127 -by (resolve_tac [EqE] 1);
  23.128 +by (rtac EqE 1);
  23.129  by (resolve_tac [absdiff_eq0_lem RS SumE] 1);
  23.130  by (TRYALL (resolve_tac prems));
  23.131  by eqintr_tac;
  23.132  by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
  23.133 -by (resolve_tac [EqE] 3  THEN  assume_tac 3);
  23.134 +by (rtac EqE 3  THEN  assume_tac 3);
  23.135  by (hyp_arith_rew_tac (prems@[add_0_right]));
  23.136  qed "absdiff_eq0";
  23.137  
  23.138 @@ -430,11 +430,11 @@
  23.139  (*for case analysis on whether a number is 0 or a successor*)
  23.140  qed_goal "iszero_decidable" Arith.thy
  23.141      "a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \
  23.142 -\		      Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
  23.143 +\                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
  23.144   (fn prems=>
  23.145    [ (NE_tac "a" 1),
  23.146 -    (resolve_tac [PlusI_inr] 3),
  23.147 -    (resolve_tac [PlusI_inl] 2),
  23.148 +    (rtac PlusI_inr 3),
  23.149 +    (rtac PlusI_inl 2),
  23.150      eqintr_tac,
  23.151      (equal_tac prems) ]);
  23.152  
  23.153 @@ -443,17 +443,17 @@
  23.154  goal Arith.thy "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
  23.155  by (NE_tac "a" 1);
  23.156  by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2])); 
  23.157 -by (resolve_tac [EqE] 1);
  23.158 +by (rtac EqE 1);
  23.159  (*case analysis on   succ(u mod b)|-|b  *)
  23.160  by (res_inst_tac [("a1", "succ(u mod b) |-| b")] 
  23.161                   (iszero_decidable RS PlusE) 1);
  23.162  by (etac SumE 3);
  23.163  by (hyp_arith_rew_tac (prems @ div_typing_rls @
  23.164 -	[modC0,modC_succ, divC0, divC_succ2])); 
  23.165 +        [modC0,modC_succ, divC0, divC_succ2])); 
  23.166  (*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
  23.167  by (resolve_tac [ add_typingL RS trans_elem ] 1);
  23.168  by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
  23.169 -by (resolve_tac [refl_elem] 3);
  23.170 +by (rtac refl_elem 3);
  23.171  by (hyp_arith_rew_tac (prems @ div_typing_rls)); 
  23.172  qed "mod_div_equality";
  23.173  
    24.1 --- a/src/CTT/Bool.ML	Mon Jan 29 13:56:41 1996 +0100
    24.2 +++ b/src/CTT/Bool.ML	Mon Jan 29 13:58:15 1996 +0100
    24.3 @@ -1,6 +1,6 @@
    24.4 -(*  Title: 	CTT/bool
    24.5 +(*  Title:      CTT/bool
    24.6      ID:         $Id$
    24.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    24.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.9      Copyright   1991  University of Cambridge
   24.10  
   24.11  Theorems for bool.thy (booleans and conditionals)
   24.12 @@ -40,7 +40,7 @@
   24.13      "!!C. [| p = q : Bool;  a = c : C(true);  b = d : C(false) |] ==> \
   24.14  \         cond(p,a,b) = cond(q,c,d) : C(p)"
   24.15   (fn _ =>
   24.16 -  [ (resolve_tac [PlusEL] 1),
   24.17 +  [ (rtac PlusEL 1),
   24.18      (REPEAT (eresolve_tac [asm_rl, refl_elem RS TEL] 1)) ]);
   24.19  
   24.20  (*computation rules for true, false*)
    25.1 --- a/src/CTT/CTT.ML	Mon Jan 29 13:56:41 1996 +0100
    25.2 +++ b/src/CTT/CTT.ML	Mon Jan 29 13:58:15 1996 +0100
    25.3 @@ -1,6 +1,6 @@
    25.4 -(*  Title: 	CTT/ctt.ML
    25.5 +(*  Title:      CTT/ctt.ML
    25.6      ID:         $Id$
    25.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    25.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.9      Copyright   1991  University of Cambridge
   25.10  
   25.11  Tactics and lemmas for ctt.thy (Constructive Type Theory)
   25.12 @@ -38,9 +38,9 @@
   25.13  qed_goal "SumIL2" CTT.thy
   25.14      "[| c=a : A;  d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)"
   25.15   (fn prems=>
   25.16 -  [ (resolve_tac [sym_elem] 1),
   25.17 -    (resolve_tac [SumIL] 1),
   25.18 -    (ALLGOALS (resolve_tac [sym_elem])),
   25.19 +  [ (rtac sym_elem 1),
   25.20 +    (rtac SumIL 1),
   25.21 +    (ALLGOALS (rtac sym_elem )),
   25.22      (ALLGOALS (resolve_tac prems)) ]);
   25.23  
   25.24  val intrL2_rls = [NI_succL, ProdIL, SumIL2, PlusI_inlL, PlusI_inrL];
   25.25 @@ -103,16 +103,16 @@
   25.26  qed_goal "replace_type" CTT.thy
   25.27      "[| B = A;  a : A |] ==> a : B"
   25.28   (fn prems=>
   25.29 -  [ (resolve_tac [equal_types] 1),
   25.30 -    (resolve_tac [sym_type] 2),
   25.31 +  [ (rtac equal_types 1),
   25.32 +    (rtac sym_type 2),
   25.33      (ALLGOALS (resolve_tac prems)) ]);
   25.34  
   25.35  (*Simplify the parameter of a unary type operator.*)
   25.36  qed_goal "subst_eqtyparg" CTT.thy
   25.37      "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
   25.38   (fn prems=>
   25.39 -  [ (resolve_tac [subst_typeL] 1),
   25.40 -    (resolve_tac [refl_type] 2),
   25.41 +  [ (rtac subst_typeL 1),
   25.42 +    (rtac refl_type 2),
   25.43      (ALLGOALS (resolve_tac prems)),
   25.44      (assume_tac 1) ]);
   25.45  
   25.46 @@ -129,25 +129,25 @@
   25.47  
   25.48  (** Tactics that instantiate CTT-rules.
   25.49      Vars in the given terms will be incremented! 
   25.50 -    The (resolve_tac [EqE] i) lets them apply to equality judgements. **)
   25.51 +    The (rtac EqE i) lets them apply to equality judgements. **)
   25.52  
   25.53  fun NE_tac (sp: string) i = 
   25.54 -  TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] NE i;
   25.55 +  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] NE i;
   25.56  
   25.57  fun SumE_tac (sp: string) i = 
   25.58 -  TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] SumE i;
   25.59 +  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] SumE i;
   25.60  
   25.61  fun PlusE_tac (sp: string) i = 
   25.62 -  TRY (resolve_tac [EqE] i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
   25.63 +  TRY (rtac EqE i) THEN res_inst_tac [ ("p",sp) ] PlusE i;
   25.64  
   25.65  (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
   25.66  
   25.67  (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
   25.68  fun add_mp_tac i = 
   25.69 -    resolve_tac [subst_prodE] i  THEN  assume_tac i  THEN  assume_tac i;
   25.70 +    rtac subst_prodE i  THEN  assume_tac i  THEN  assume_tac i;
   25.71  
   25.72  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   25.73 -fun mp_tac i = eresolve_tac [subst_prodE] i  THEN  assume_tac i;
   25.74 +fun mp_tac i = etac subst_prodE i  THEN  assume_tac i;
   25.75  
   25.76  (*"safe" when regarded as predicate calculus rules*)
   25.77  val safe_brls = sort lessb 
    26.1 --- a/src/CTT/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
    26.2 +++ b/src/CTT/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
    26.3 @@ -1,6 +1,6 @@
    26.4 -(*  Title: 	CTT/ROOT
    26.5 +(*  Title:      CTT/ROOT
    26.6      ID:         $Id$
    26.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    26.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    26.9      Copyright   1991  University of Cambridge
   26.10  
   26.11  Adds Constructive Type Theory to a database containing pure Isabelle. 
   26.12 @@ -23,4 +23,4 @@
   26.13  use "../Pure/install_pp.ML";
   26.14  print_depth 8;
   26.15  
   26.16 -val CTT_build_completed = ();	(*indicate successful build*)
   26.17 +val CTT_build_completed = ();   (*indicate successful build*)
    27.1 --- a/src/CTT/ex/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
    27.2 +++ b/src/CTT/ex/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
    27.3 @@ -1,6 +1,6 @@
    27.4 -(*  Title: 	CTT/ex/ROOT
    27.5 +(*  Title:      CTT/ex/ROOT
    27.6      ID:         $Id$
    27.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    27.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    27.9      Copyright   1991  University of Cambridge
   27.10  
   27.11  Executes all examples for Constructive Type Theory. 
    28.1 --- a/src/CTT/ex/equal.ML	Mon Jan 29 13:56:41 1996 +0100
    28.2 +++ b/src/CTT/ex/equal.ML	Mon Jan 29 13:58:15 1996 +0100
    28.3 @@ -1,6 +1,6 @@
    28.4 -(*  Title: 	CTT/ex/equal
    28.5 +(*  Title:      CTT/ex/equal
    28.6      ID:         $Id$
    28.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    28.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    28.9      Copyright   1991  University of Cambridge
   28.10  
   28.11  Equality reasoning by rewriting.
    29.1 --- a/src/CTT/ex/synth.ML	Mon Jan 29 13:56:41 1996 +0100
    29.2 +++ b/src/CTT/ex/synth.ML	Mon Jan 29 13:58:15 1996 +0100
    29.3 @@ -1,6 +1,6 @@
    29.4 -(*  Title: 	CTT/ex/synth
    29.5 +(*  Title:      CTT/ex/synth
    29.6      ID:         $Id$
    29.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    29.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    29.9      Copyright   1991  University of Cambridge
   29.10  *)
   29.11  
   29.12 @@ -9,8 +9,8 @@
   29.13  
   29.14  writeln"discovery of predecessor function";
   29.15  goal CTT.thy 
   29.16 - "?a : SUM pred:?A . Eq(N, pred`0, 0)	\
   29.17 -\		  *  (PROD n:N. Eq(N, pred ` succ(n), n))";
   29.18 + "?a : SUM pred:?A . Eq(N, pred`0, 0)   \
   29.19 +\                 *  (PROD n:N. Eq(N, pred ` succ(n), n))";
   29.20  by (intr_tac[]);
   29.21  by eqintr_tac;
   29.22  by (resolve_tac reduction_rls 3);
   29.23 @@ -36,7 +36,7 @@
   29.24    See following example.*)
   29.25  goal CTT.thy 
   29.26      "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)  \
   29.27 -\  	          * Eq(?A, ?b(inr(i)), <succ(0), i>)";
   29.28 +\                 * Eq(?A, ?b(inr(i)), <succ(0), i>)";
   29.29  by (intr_tac[]);
   29.30  by eqintr_tac;
   29.31  by (resolve_tac comp_rls 1);
   29.32 @@ -49,13 +49,13 @@
   29.33   Simpler still: make ?A into a constant type N*N.*)
   29.34  goal CTT.thy 
   29.35      "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)   \
   29.36 -\ 	         *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
   29.37 +\                *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
   29.38  
   29.39  writeln"A tricky combination of when and split";
   29.40  (*Now handled easily, but caused great problems once*)
   29.41  goal CTT.thy 
   29.42      "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)   \
   29.43 -\  	    	           *  Eq(?A, ?b(inr(<i,j>)), j)";
   29.44 +\                          *  Eq(?A, ?b(inr(<i,j>)), j)";
   29.45  by (intr_tac[]); 
   29.46  by eqintr_tac;
   29.47  by (resolve_tac [ PlusC_inl RS trans_elem ] 1);
   29.48 @@ -69,18 +69,18 @@
   29.49  (*similar but allows the type to depend on i and j*)
   29.50  goal CTT.thy 
   29.51      "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
   29.52 -\ 	    	          *   Eq(?A(i,j), ?b(inr(<i,j>)), j)";
   29.53 +\                         *   Eq(?A(i,j), ?b(inr(<i,j>)), j)";
   29.54  
   29.55  (*similar but specifying the type N simplifies the unification problems*)
   29.56  goal CTT.thy
   29.57 -    "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)	\
   29.58 -\ 	    	          *   Eq(N, ?b(inr(<i,j>)), j)";
   29.59 +    "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)  \
   29.60 +\                         *   Eq(N, ?b(inr(<i,j>)), j)";
   29.61  
   29.62  
   29.63  writeln"Deriving the addition operator";
   29.64  goal Arith.thy 
   29.65     "?c : PROD n:N. Eq(N, ?f(0,n), n)  \
   29.66 -\  	        *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
   29.67 +\               *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
   29.68  by (intr_tac[]);
   29.69  by eqintr_tac;
   29.70  by (resolve_tac comp_rls 1);
   29.71 @@ -91,8 +91,8 @@
   29.72  writeln"The addition function -- using explicit lambdas";
   29.73  goal Arith.thy 
   29.74    "?c : SUM plus : ?A .  \
   29.75 -\  	 PROD x:N. Eq(N, plus`0`x, x)  \
   29.76 -\  	        *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
   29.77 +\        PROD x:N. Eq(N, plus`0`x, x)  \
   29.78 +\               *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
   29.79  by (intr_tac[]);
   29.80  by eqintr_tac;
   29.81  by (resolve_tac [TSimp.split_eqn] 3);
    30.1 --- a/src/CTT/ex/typechk.ML	Mon Jan 29 13:56:41 1996 +0100
    30.2 +++ b/src/CTT/ex/typechk.ML	Mon Jan 29 13:58:15 1996 +0100
    30.3 @@ -1,6 +1,6 @@
    30.4 -(*  Title: 	CTT/ex/typechk
    30.5 +(*  Title:      CTT/ex/typechk
    30.6      ID:         $Id$
    30.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    30.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    30.9      Copyright   1991  University of Cambridge
   30.10    
   30.11  Easy examples: type checking and type deduction
    31.1 --- a/src/CTT/rew.ML	Mon Jan 29 13:56:41 1996 +0100
    31.2 +++ b/src/CTT/rew.ML	Mon Jan 29 13:58:15 1996 +0100
    31.3 @@ -1,6 +1,6 @@
    31.4 -(*  Title: 	CTT/rew
    31.5 +(*  Title:      CTT/rew
    31.6      ID:         $Id$
    31.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    31.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    31.9      Copyright   1991  University of Cambridge
   31.10  
   31.11  Simplifier for CTT, using Typedsimp
   31.12 @@ -17,14 +17,14 @@
   31.13  
   31.14  structure TSimp_data: TSIMP_DATA =
   31.15    struct
   31.16 -  val refl		= refl_elem
   31.17 -  val sym		= sym_elem
   31.18 -  val trans		= trans_elem
   31.19 -  val refl_red		= refl_red
   31.20 -  val trans_red		= trans_red
   31.21 -  val red_if_equal	= red_if_equal
   31.22 -  val default_rls 	= comp_rls
   31.23 -  val routine_tac 	= routine_tac routine_rls
   31.24 +  val refl              = refl_elem
   31.25 +  val sym               = sym_elem
   31.26 +  val trans             = trans_elem
   31.27 +  val refl_red          = refl_red
   31.28 +  val trans_red         = trans_red
   31.29 +  val red_if_equal      = red_if_equal
   31.30 +  val default_rls       = comp_rls
   31.31 +  val routine_tac       = routine_tac routine_rls
   31.32    end;
   31.33  
   31.34  structure TSimp = TSimpFun (TSimp_data);
    32.1 --- a/src/Cube/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
    32.2 +++ b/src/Cube/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
    32.3 @@ -1,6 +1,6 @@
    32.4 -(*  Title: 	Cube/ROOT
    32.5 +(*  Title:      Cube/ROOT
    32.6      ID:         $Id$
    32.7 -    Author: 	Tobias Nipkow
    32.8 +    Author:     Tobias Nipkow
    32.9      Copyright   1992  University of Cambridge
   32.10  
   32.11  The Lambda-Cube a la Barendregt
   32.12 @@ -17,4 +17,4 @@
   32.13  use "../Pure/install_pp.ML";
   32.14  print_depth 8;
   32.15  
   32.16 -val Cube_build_completed = ();	(*indicate successful build*)
   32.17 +val Cube_build_completed = ();  (*indicate successful build*)
    33.1 --- a/src/Cube/ex.ML	Mon Jan 29 13:56:41 1996 +0100
    33.2 +++ b/src/Cube/ex.ML	Mon Jan 29 13:58:15 1996 +0100
    33.3 @@ -1,6 +1,6 @@
    33.4  (* Examples taken from
    33.5 -	H. Barendregt. Introduction to Generalised Type Systems.
    33.6 -	J. Functional Programming.
    33.7 +        H. Barendregt. Introduction to Generalised Type Systems.
    33.8 +        J. Functional Programming.
    33.9  *)
   33.10  
   33.11  Cube_build_completed;    (*Cause examples to fail if Cube did*)
   33.12 @@ -11,11 +11,11 @@
   33.13      REPEAT(resolve_tac[strip_b,strip_s]i THEN DEPTH_SOLVE_1(ares_tac thms i));
   33.14  
   33.15  val imp_elim = prove_goal thy "[| f:A->B; a:A; f^a:B ==> PROP P |] ==> PROP P"
   33.16 -	(fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
   33.17 +        (fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
   33.18  
   33.19  val pi_elim = prove_goal thy
   33.20 -	"[| F:Prod(A,B); a:A; F^a:B(a) ==> PROP P |] ==> PROP P"
   33.21 -	(fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
   33.22 +        "[| F:Prod(A,B); a:A; F^a:B(a) ==> PROP P |] ==> PROP P"
   33.23 +        (fn asms => [REPEAT(resolve_tac (app::asms) 1)]);
   33.24  
   33.25  (* SIMPLE TYPES *)
   33.26  
   33.27 @@ -114,7 +114,7 @@
   33.28  uresult();
   33.29  
   33.30  goal LP_thy "A:* P:A->* Q:* a0:A |- \
   33.31 -\	Lam x:Pi a:A.P^a->Q. Lam y:Pi a:A.P^a. x^a0^(y^a0): ?T";
   33.32 +\       Lam x:Pi a:A.P^a->Q. Lam y:Pi a:A.P^a. x^a0^(y^a0): ?T";
   33.33  by (DEPTH_SOLVE (ares_tac LP 1));
   33.34  uresult();
   33.35  
   33.36 @@ -157,13 +157,13 @@
   33.37  uresult();
   33.38  
   33.39  goal LP2_thy "A:* P:A->A->* |- \
   33.40 -\	(Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P : ?T";
   33.41 +\       (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P : ?T";
   33.42  by (DEPTH_SOLVE (ares_tac LP2 1));
   33.43  uresult();
   33.44  
   33.45  (* Antisymmetry implies irreflexivity: *)
   33.46  goal LP2_thy "A:* P:A->A->* |- \
   33.47 -\	?p: (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P";
   33.48 +\       ?p: (Pi a:A.Pi b:A.P^a^b->P^b^a->Pi P:*.P) -> Pi a:A.P^a^a->Pi P:*.P";
   33.49  by (strip_asms_tac LP2 1);
   33.50  by (rtac lam_ss 1);
   33.51  by (DEPTH_SOLVE_1(ares_tac LP2 1));
   33.52 @@ -208,12 +208,12 @@
   33.53  (* Some random examples *)
   33.54  
   33.55  goal LP2_thy "A:* c:A f:A->A |- \
   33.56 -\	Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
   33.57 +\       Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
   33.58  by (DEPTH_SOLVE(ares_tac LP2 1));
   33.59  uresult();
   33.60  
   33.61  goal CC_thy "Lam A:*.Lam c:A.Lam f:A->A. \
   33.62 -\	Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
   33.63 +\       Lam a:A. Pi P:A->*.P^c -> (Pi x:A. P^x->P^(f^x)) -> P^a : ?T";
   33.64  by (DEPTH_SOLVE(ares_tac CC 1));
   33.65  uresult();
   33.66  
    34.1 --- a/src/FOL/FOL.ML	Mon Jan 29 13:56:41 1996 +0100
    34.2 +++ b/src/FOL/FOL.ML	Mon Jan 29 13:58:15 1996 +0100
    34.3 @@ -1,6 +1,6 @@
    34.4 -(*  Title: 	FOL/FOL.ML
    34.5 +(*  Title:      FOL/FOL.ML
    34.6      ID:         $Id$
    34.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    34.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    34.9      Copyright   1991  University of Cambridge
   34.10  
   34.11  Tactics and lemmas for FOL.thy (classical First-Order Logic)
   34.12 @@ -14,7 +14,7 @@
   34.13  qed_goal "disjCI" FOL.thy 
   34.14     "(~Q ==> P) ==> P|Q"
   34.15   (fn prems=>
   34.16 -  [ (resolve_tac [classical] 1),
   34.17 +  [ (rtac classical 1),
   34.18      (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
   34.19      (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
   34.20  
   34.21 @@ -22,17 +22,17 @@
   34.22  qed_goal "ex_classical" FOL.thy 
   34.23     "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
   34.24   (fn prems=>
   34.25 -  [ (resolve_tac [classical] 1),
   34.26 +  [ (rtac classical 1),
   34.27      (eresolve_tac (prems RL [exI]) 1) ]);
   34.28  
   34.29  (*version of above, simplifying ~EX to ALL~ *)
   34.30  qed_goal "exCI" FOL.thy 
   34.31     "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
   34.32   (fn [prem]=>
   34.33 -  [ (resolve_tac [ex_classical] 1),
   34.34 +  [ (rtac ex_classical 1),
   34.35      (resolve_tac [notI RS allI RS prem] 1),
   34.36 -    (eresolve_tac [notE] 1),
   34.37 -    (eresolve_tac [exI] 1) ]);
   34.38 +    (etac notE 1),
   34.39 +    (etac exI 1) ]);
   34.40  
   34.41  qed_goal "excluded_middle" FOL.thy "~P | P"
   34.42   (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
   34.43 @@ -54,7 +54,7 @@
   34.44  (*Double negation law*)
   34.45  qed_goal "notnotD" FOL.thy "~~P ==> P"
   34.46   (fn [major]=>
   34.47 -  [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
   34.48 +  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
   34.49  
   34.50  
   34.51  (*** Tactics for implication and contradiction ***)
   34.52 @@ -64,6 +64,6 @@
   34.53  qed_goalw "iffCE" FOL.thy [iff_def]
   34.54      "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
   34.55   (fn prems =>
   34.56 -  [ (resolve_tac [conjE] 1),
   34.57 +  [ (rtac conjE 1),
   34.58      (REPEAT (DEPTH_SOLVE_1 
   34.59 -	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
   34.60 +        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
    35.1 --- a/src/FOL/IFOL.ML	Mon Jan 29 13:56:41 1996 +0100
    35.2 +++ b/src/FOL/IFOL.ML	Mon Jan 29 13:58:15 1996 +0100
    35.3 @@ -1,6 +1,6 @@
    35.4 -(*  Title: 	FOL/IFOL.ML
    35.5 +(*  Title:      FOL/IFOL.ML
    35.6      ID:         $Id$
    35.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    35.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    35.9      Copyright   1992  University of Cambridge
   35.10  
   35.11  Tactics and lemmas for IFOL.thy (intuitionistic first-order logic)
   35.12 @@ -85,7 +85,7 @@
   35.13  (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   35.14  qed_goalw "iffE" IFOL.thy [iff_def]
   35.15      "[| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R"
   35.16 - (fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]);
   35.17 + (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);
   35.18  
   35.19  (* Destruct rules for <-> similar to Modus Ponens *)
   35.20  
   35.21 @@ -125,7 +125,7 @@
   35.22  qed_goal "ex_ex1I" IFOL.thy
   35.23      "[| EX x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
   35.24   (fn [ex,eq] => [ (rtac (ex RS exE) 1),
   35.25 -		  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
   35.26 +                  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
   35.27  
   35.28  qed_goalw "ex1E" IFOL.thy [ex1_def]
   35.29      "[| EX! x.P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
   35.30 @@ -171,14 +171,14 @@
   35.31   (fn prems =>
   35.32    [ (cut_facts_tac prems 1),
   35.33      (REPEAT   (ares_tac [iffI,impI] 1
   35.34 -      ORELSE  eresolve_tac [iffE] 1
   35.35 +      ORELSE  etac iffE 1
   35.36        ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
   35.37  
   35.38  qed_goal "iff_cong" IFOL.thy 
   35.39      "[| P <-> P';  Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
   35.40   (fn prems =>
   35.41    [ (cut_facts_tac prems 1),
   35.42 -    (REPEAT   (eresolve_tac [iffE] 1
   35.43 +    (REPEAT   (etac iffE 1
   35.44        ORELSE  ares_tac [iffI] 1
   35.45        ORELSE  mp_tac 1)) ]);
   35.46  
   35.47 @@ -195,12 +195,12 @@
   35.48   (fn prems =>
   35.49    [ (REPEAT   (ares_tac [iffI,allI] 1
   35.50        ORELSE   mp_tac 1
   35.51 -      ORELSE   eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]);
   35.52 +      ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
   35.53  
   35.54  qed_goal "ex_cong" IFOL.thy 
   35.55      "(!!x.P(x) <-> Q(x)) ==> (EX x.P(x)) <-> (EX x.Q(x))"
   35.56   (fn prems =>
   35.57 -  [ (REPEAT   (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1
   35.58 +  [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   35.59        ORELSE   mp_tac 1
   35.60        ORELSE   iff_tac prems 1)) ]);
   35.61  
   35.62 @@ -241,7 +241,7 @@
   35.63     "[| a=b |]  ==>  t(a)=t(b)"
   35.64   (fn prems=>
   35.65    [ (resolve_tac (prems RL [ssubst]) 1),
   35.66 -    (resolve_tac [refl] 1) ]);
   35.67 +    (rtac refl 1) ]);
   35.68  
   35.69  qed_goal "subst_context2" IFOL.thy 
   35.70     "[| a=b;  c=d |]  ==>  t(a,c)=t(b,d)"
   35.71 @@ -254,23 +254,23 @@
   35.72    [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   35.73  
   35.74  (*Useful with eresolve_tac for proving equalties from known equalities.
   35.75 -	a = b
   35.76 -	|   |
   35.77 -	c = d	*)
   35.78 +        a = b
   35.79 +        |   |
   35.80 +        c = d   *)
   35.81  qed_goal "box_equals" IFOL.thy
   35.82      "[| a=b;  a=c;  b=d |] ==> c=d"  
   35.83   (fn prems=>
   35.84 -  [ (resolve_tac [trans] 1),
   35.85 -    (resolve_tac [trans] 1),
   35.86 -    (resolve_tac [sym] 1),
   35.87 +  [ (rtac trans 1),
   35.88 +    (rtac trans 1),
   35.89 +    (rtac sym 1),
   35.90      (REPEAT (resolve_tac prems 1)) ]);
   35.91  
   35.92  (*Dual of box_equals: for proving equalities backwards*)
   35.93  qed_goal "simp_equals" IFOL.thy
   35.94      "[| a=c;  b=d;  c=d |] ==> a=b"  
   35.95   (fn prems=>
   35.96 -  [ (resolve_tac [trans] 1),
   35.97 -    (resolve_tac [trans] 1),
   35.98 +  [ (rtac trans 1),
   35.99 +    (rtac trans 1),
  35.100      (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]);
  35.101  
  35.102  (** Congruence rules for predicate letters **)
  35.103 @@ -300,9 +300,9 @@
  35.104  
  35.105  val pred_congs = 
  35.106      flat (map (fn c => 
  35.107 -	       map (fn th => read_instantiate [("P",c)] th)
  35.108 -		   [pred1_cong,pred2_cong,pred3_cong])
  35.109 -	       (explode"PQRS"));
  35.110 +               map (fn th => read_instantiate [("P",c)] th)
  35.111 +                   [pred1_cong,pred2_cong,pred3_cong])
  35.112 +               (explode"PQRS"));
  35.113  
  35.114  (*special case for the equality predicate!*)
  35.115  val eq_cong = read_instantiate [("P","op =")] pred2_cong;
  35.116 @@ -360,6 +360,6 @@
  35.117  
  35.118  (*Courtesy Krzysztof Grabczewski*)
  35.119  val major::prems = goal IFOL.thy "[| P|Q;  P==>R;  Q==>S |] ==> R|S";
  35.120 -br (major RS disjE) 1;
  35.121 +by (rtac (major RS disjE) 1);
  35.122  by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
  35.123  qed "disj_imp_disj";
    36.1 --- a/src/FOL/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
    36.2 +++ b/src/FOL/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
    36.3 @@ -1,6 +1,6 @@
    36.4 -(*  Title: 	FOL/ROOT
    36.5 +(*  Title:      FOL/ROOT
    36.6      ID:         $Id$
    36.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    36.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    36.9      Copyright   1993  University of Cambridge
   36.10  
   36.11  Adds First-Order Logic to a database containing pure Isabelle. 
   36.12 @@ -43,10 +43,10 @@
   36.13  (*** Applying ClassicalFun to create a classical prover ***)
   36.14  structure Classical_Data = 
   36.15    struct
   36.16 -  val sizef	= size_of_thm
   36.17 -  val mp	= mp
   36.18 -  val not_elim	= notE
   36.19 -  val classical	= classical
   36.20 +  val sizef     = size_of_thm
   36.21 +  val mp        = mp
   36.22 +  val not_elim  = notE
   36.23 +  val classical = classical
   36.24    val hyp_subst_tacs=[hyp_subst_tac]
   36.25    end;
   36.26  
   36.27 @@ -72,4 +72,4 @@
   36.28  use "../Pure/install_pp.ML";
   36.29  print_depth 8;
   36.30  
   36.31 -val FOL_build_completed = ();	(*indicate successful build*)
   36.32 +val FOL_build_completed = ();   (*indicate successful build*)
    37.1 --- a/src/FOL/ex/If.ML	Mon Jan 29 13:56:41 1996 +0100
    37.2 +++ b/src/FOL/ex/If.ML	Mon Jan 29 13:58:15 1996 +0100
    37.3 @@ -1,6 +1,6 @@
    37.4 -(*  Title: 	FOL/ex/if
    37.5 +(*  Title:      FOL/ex/if
    37.6      ID:         $Id$
    37.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    37.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    37.9      Copyright   1991  University of Cambridge
   37.10  
   37.11  For ex/if.thy.  First-Order Logic: the 'if' example
   37.12 @@ -23,11 +23,11 @@
   37.13  
   37.14  goal If.thy
   37.15      "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
   37.16 -by (resolve_tac [iffI] 1);
   37.17 -by (eresolve_tac [ifE] 1);
   37.18 -by (eresolve_tac [ifE] 1);
   37.19 -by (resolve_tac [ifI] 1);
   37.20 -by (resolve_tac [ifI] 1);
   37.21 +by (rtac iffI 1);
   37.22 +by (etac ifE 1);
   37.23 +by (etac ifE 1);
   37.24 +by (rtac ifI 1);
   37.25 +by (rtac ifI 1);
   37.26  
   37.27  choplev 0;
   37.28  val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
   37.29 @@ -40,7 +40,7 @@
   37.30  qed "nested_ifs";
   37.31  
   37.32  choplev 0;
   37.33 -by (rewrite_goals_tac [if_def]);
   37.34 +by (rewtac if_def);
   37.35  by (fast_tac FOL_cs 1);
   37.36  result();
   37.37  
   37.38 @@ -53,7 +53,7 @@
   37.39  by (REPEAT (step_tac if_cs 1));
   37.40  
   37.41  choplev 0;
   37.42 -by (rewrite_goals_tac [if_def]);
   37.43 +by (rewtac if_def);
   37.44  by (fast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected";
   37.45  (*Check that subgoals remain: proof failed.*)
   37.46  getgoal 1; 
    38.1 --- a/src/FOL/ex/List.ML	Mon Jan 29 13:56:41 1996 +0100
    38.2 +++ b/src/FOL/ex/List.ML	Mon Jan 29 13:58:15 1996 +0100
    38.3 @@ -1,6 +1,6 @@
    38.4 -(*  Title: 	FOL/ex/list
    38.5 +(*  Title:      FOL/ex/list
    38.6      ID:         $Id$
    38.7 -    Author: 	Tobias Nipkow
    38.8 +    Author:     Tobias Nipkow
    38.9      Copyright   1991  University of Cambridge
   38.10  
   38.11  For ex/list.thy.  Examples of simplification and induction on lists
   38.12 @@ -14,8 +14,8 @@
   38.13  qed "list_exh";
   38.14  
   38.15  val list_rew_thms = [list_distinct1,list_distinct2,app_nil,app_cons,
   38.16 -		     hd_eq,tl_eq,forall_nil,forall_cons,list_free,
   38.17 -		     len_nil,len_cons,at_0,at_succ];
   38.18 +                     hd_eq,tl_eq,forall_nil,forall_cons,list_free,
   38.19 +                     len_nil,len_cons,at_0,at_succ];
   38.20  
   38.21  val list_ss = nat_ss addsimps list_rew_thms;
   38.22  
    39.1 --- a/src/FOL/ex/Nat.ML	Mon Jan 29 13:56:41 1996 +0100
    39.2 +++ b/src/FOL/ex/Nat.ML	Mon Jan 29 13:58:15 1996 +0100
    39.3 @@ -1,6 +1,6 @@
    39.4 -(*  Title: 	FOL/ex/nat.ML
    39.5 +(*  Title:      FOL/ex/nat.ML
    39.6      ID:         $Id$
    39.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    39.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    39.9      Copyright   1992  University of Cambridge
   39.10  
   39.11  Examples for the manual "Introduction to Isabelle"
   39.12 @@ -17,17 +17,17 @@
   39.13  
   39.14  goal Nat.thy "Suc(k) ~= k";
   39.15  by (res_inst_tac [("n","k")] induct 1);
   39.16 -by (resolve_tac [notI] 1);
   39.17 -by (eresolve_tac [Suc_neq_0] 1);
   39.18 -by (resolve_tac [notI] 1);
   39.19 -by (eresolve_tac [notE] 1);
   39.20 -by (eresolve_tac [Suc_inject] 1);
   39.21 +by (rtac notI 1);
   39.22 +by (etac Suc_neq_0 1);
   39.23 +by (rtac notI 1);
   39.24 +by (etac notE 1);
   39.25 +by (etac Suc_inject 1);
   39.26  qed "Suc_n_not_n";
   39.27  
   39.28  
   39.29  goal Nat.thy "(k+m)+n = k+(m+n)";
   39.30  prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
   39.31 -by (resolve_tac [induct] 1);
   39.32 +by (rtac induct 1);
   39.33  back();
   39.34  back();
   39.35  back();
   39.36 @@ -36,11 +36,11 @@
   39.37  back();
   39.38  
   39.39  goalw Nat.thy [add_def] "0+n = n";
   39.40 -by (resolve_tac [rec_0] 1);
   39.41 +by (rtac rec_0 1);
   39.42  qed "add_0";
   39.43  
   39.44  goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
   39.45 -by (resolve_tac [rec_Suc] 1);
   39.46 +by (rtac rec_Suc 1);
   39.47  qed "add_Suc";
   39.48  
   39.49  val add_ss = FOL_ss addsimps [add_0, add_Suc];
    40.1 --- a/src/FOL/ex/Nat2.ML	Mon Jan 29 13:56:41 1996 +0100
    40.2 +++ b/src/FOL/ex/Nat2.ML	Mon Jan 29 13:58:15 1996 +0100
    40.3 @@ -1,6 +1,6 @@
    40.4 -(*  Title: 	FOL/ex/nat2.ML
    40.5 +(*  Title:      FOL/ex/nat2.ML
    40.6      ID:         $Id$
    40.7 -    Author: 	Tobias Nipkow
    40.8 +    Author:     Tobias Nipkow
    40.9      Copyright   1991  University of Cambridge
   40.10  
   40.11  For ex/nat.thy.  
   40.12 @@ -10,9 +10,9 @@
   40.13  open Nat2;
   40.14  
   40.15  val nat_rews = [pred_0, pred_succ, plus_0, plus_succ, 
   40.16 -		    nat_distinct1, nat_distinct2, succ_inject,
   40.17 -		    leq_0,leq_succ_succ,leq_succ_0, 
   40.18 -		    lt_0_succ,lt_succ_succ,lt_0];
   40.19 +                    nat_distinct1, nat_distinct2, succ_inject,
   40.20 +                    leq_0,leq_succ_succ,leq_succ_0, 
   40.21 +                    lt_0_succ,lt_succ_succ,lt_0];
   40.22  
   40.23  val nat_ss = FOL_ss addsimps nat_rews;
   40.24  
    41.1 --- a/src/FOL/ex/NatClass.ML	Mon Jan 29 13:56:41 1996 +0100
    41.2 +++ b/src/FOL/ex/NatClass.ML	Mon Jan 29 13:58:15 1996 +0100
    41.3 @@ -1,6 +1,6 @@
    41.4 -(*  Title: 	FOL/ex/NatClass.ML
    41.5 +(*  Title:      FOL/ex/NatClass.ML
    41.6      ID:         $Id$
    41.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    41.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    41.9      Copyright   1992  University of Cambridge
   41.10  
   41.11  This is Nat.ML trivially modified to make it work with NatClass.thy.
   41.12 @@ -10,17 +10,17 @@
   41.13  
   41.14  goal NatClass.thy "Suc(k) ~= (k::'a::nat)";
   41.15  by (res_inst_tac [("n","k")] induct 1);
   41.16 -by (resolve_tac [notI] 1);
   41.17 -by (eresolve_tac [Suc_neq_0] 1);
   41.18 -by (resolve_tac [notI] 1);
   41.19 -by (eresolve_tac [notE] 1);
   41.20 -by (eresolve_tac [Suc_inject] 1);
   41.21 +by (rtac notI 1);
   41.22 +by (etac Suc_neq_0 1);
   41.23 +by (rtac notI 1);
   41.24 +by (etac notE 1);
   41.25 +by (etac Suc_inject 1);
   41.26  qed "Suc_n_not_n";
   41.27  
   41.28  
   41.29  goal NatClass.thy "(k+m)+n = k+(m+n)";
   41.30  prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
   41.31 -by (resolve_tac [induct] 1);
   41.32 +by (rtac induct 1);
   41.33  back();
   41.34  back();
   41.35  back();
   41.36 @@ -29,11 +29,11 @@
   41.37  back();
   41.38  
   41.39  goalw NatClass.thy [add_def] "0+n = n";
   41.40 -by (resolve_tac [rec_0] 1);
   41.41 +by (rtac rec_0 1);
   41.42  qed "add_0";
   41.43  
   41.44  goalw NatClass.thy [add_def] "Suc(m)+n = Suc(m+n)";
   41.45 -by (resolve_tac [rec_Suc] 1);
   41.46 +by (rtac rec_Suc 1);
   41.47  qed "add_Suc";
   41.48  
   41.49  val add_ss = FOL_ss addsimps [add_0, add_Suc];
    42.1 --- a/src/FOL/ex/Prolog.ML	Mon Jan 29 13:56:41 1996 +0100
    42.2 +++ b/src/FOL/ex/Prolog.ML	Mon Jan 29 13:58:15 1996 +0100
    42.3 @@ -1,6 +1,6 @@
    42.4 -(*  Title: 	FOL/ex/prolog.ML
    42.5 +(*  Title:      FOL/ex/prolog.ML
    42.6      ID:         $Id$
    42.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    42.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    42.9      Copyright   1992  University of Cambridge
   42.10  
   42.11  For ex/prolog.thy.  First-Order Logic: PROLOG examples
    43.1 --- a/src/FOL/ex/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
    43.2 +++ b/src/FOL/ex/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
    43.3 @@ -1,6 +1,6 @@
    43.4 -(*  Title: 	FOL/ex/ROOT
    43.5 +(*  Title:      FOL/ex/ROOT
    43.6      ID:         $Id$
    43.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    43.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    43.9      Copyright   1992  University of Cambridge
   43.10  
   43.11  Executes all examples for First-Order Logic. 
   43.12 @@ -8,7 +8,7 @@
   43.13  
   43.14  writeln"Root file for FOL examples";
   43.15  
   43.16 -FOL_build_completed;	(*Cause examples to fail if FOL did*)
   43.17 +FOL_build_completed;    (*Cause examples to fail if FOL did*)
   43.18  
   43.19  proof_timing := true;
   43.20  
    44.1 --- a/src/FOL/ex/cla.ML	Mon Jan 29 13:56:41 1996 +0100
    44.2 +++ b/src/FOL/ex/cla.ML	Mon Jan 29 13:58:15 1996 +0100
    44.3 @@ -1,6 +1,6 @@
    44.4 -(*  Title: 	FOL/ex/cla
    44.5 +(*  Title:      FOL/ex/cla
    44.6      ID:         $Id$
    44.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    44.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    44.9      Copyright   1994  University of Cambridge
   44.10  
   44.11  Classical First-Order Logic
   44.12 @@ -222,8 +222,8 @@
   44.13  result();
   44.14  
   44.15  writeln"Problem 26";
   44.16 -goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) &	\
   44.17 -\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))	\
   44.18 +goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) & \
   44.19 +\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
   44.20  \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
   44.21  by (fast_tac FOL_cs 1);
   44.22  result();
   44.23 @@ -283,9 +283,9 @@
   44.24  
   44.25  writeln"Problem 34  AMENDED (TWICE!!)";
   44.26  (*Andrews's challenge*)
   44.27 -goal FOL.thy "((EX x. ALL y. p(x) <-> p(y))  <->		\
   44.28 -\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->	\
   44.29 -\             ((EX x. ALL y. q(x) <-> q(y))  <->		\
   44.30 +goal FOL.thy "((EX x. ALL y. p(x) <-> p(y))  <->                \
   44.31 +\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
   44.32 +\             ((EX x. ALL y. q(x) <-> q(y))  <->                \
   44.33  \              ((EX x. p(x)) <-> (ALL y. q(y))))";
   44.34  by (deepen_tac FOL_cs 0 1);
   44.35  result();
   44.36 @@ -318,10 +318,10 @@
   44.37  
   44.38  writeln"Problem 38";
   44.39  goal FOL.thy
   44.40 -    "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->	\
   44.41 -\            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->		\
   44.42 -\    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &	\
   44.43 -\            (~p(a) | ~(EX y. p(y) & r(x,y)) |				\
   44.44 +    "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
   44.45 +\            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
   44.46 +\    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
   44.47 +\            (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
   44.48  \             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
   44.49  by (fast_tac FOL_cs 1);
   44.50  result();
   44.51 @@ -338,7 +338,7 @@
   44.52  result();
   44.53  
   44.54  writeln"Problem 41";
   44.55 -goal FOL.thy "(ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))	\
   44.56 +goal FOL.thy "(ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))        \
   44.57  \         --> ~ (EX z. ALL x. f(x,z))";
   44.58  by (fast_tac FOL_cs 1);
   44.59  result();
   44.60 @@ -349,29 +349,29 @@
   44.61  result();
   44.62  
   44.63  writeln"Problem 43";
   44.64 -goal FOL.thy "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y)))	\
   44.65 +goal FOL.thy "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y)))     \
   44.66  \         --> (ALL x. ALL y. q(x,y) <-> q(y,x))";
   44.67  by (mini_tac 1);
   44.68  by (deepen_tac FOL_cs 5 1);
   44.69  (*Faster alternative proof!
   44.70 -	by (asm_simp_tac FOL_ss 1); by (fast_tac FOL_cs 1);	
   44.71 +        by (asm_simp_tac FOL_ss 1); by (fast_tac FOL_cs 1);     
   44.72  *)
   44.73  result();
   44.74  
   44.75  writeln"Problem 44";
   44.76 -goal FOL.thy "(ALL x. f(x) -->						\
   44.77 -\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &   	\
   44.78 -\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))			\
   44.79 +goal FOL.thy "(ALL x. f(x) -->                                          \
   44.80 +\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
   44.81 +\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
   44.82  \             --> (EX x. j(x) & ~f(x))";
   44.83  by (fast_tac FOL_cs 1);
   44.84  result();
   44.85  
   44.86  writeln"Problem 45";
   44.87 -goal FOL.thy "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))	\
   44.88 -\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &	\
   44.89 -\     ~ (EX y. l(y) & k(y)) &					\
   44.90 -\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))			\
   44.91 -\                 & (ALL y. g(y) & h(x,y) --> j(x,y)))		\
   44.92 +goal FOL.thy "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))  \
   44.93 +\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &    \
   44.94 +\     ~ (EX y. l(y) & k(y)) &                                   \
   44.95 +\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
   44.96 +\                 & (ALL y. g(y) & h(x,y) --> j(x,y)))          \
   44.97  \     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
   44.98  by (best_tac FOL_cs 1); 
   44.99  result();
  44.100 @@ -388,12 +388,12 @@
  44.101  (*Hard because it involves substitution for Vars;
  44.102    the type constraint ensures that x,y,z have the same type as a,b,u. *)
  44.103  goal FOL.thy "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \
  44.104 -\		--> (ALL u::'a.P(u))";
  44.105 +\               --> (ALL u::'a.P(u))";
  44.106  by (safe_tac FOL_cs);
  44.107  by (res_inst_tac [("x","a")] allE 1);
  44.108 -ba 1;
  44.109 +by (assume_tac 1);
  44.110  by (res_inst_tac [("x","b")] allE 1);
  44.111 -ba 1;
  44.112 +by (assume_tac 1);
  44.113  by (fast_tac FOL_cs 1);
  44.114  result();
  44.115  
  44.116 @@ -437,8 +437,8 @@
  44.117  \  killed(?who,agatha)";
  44.118  by (safe_tac FOL_cs);
  44.119  by (dres_inst_tac [("x1","x")] (spec RS mp) 1);
  44.120 -ba 1;
  44.121 -be (spec RS exE) 1;
  44.122 +by (assume_tac 1);
  44.123 +by (etac (spec RS exE) 1);
  44.124  by (REPEAT (etac allE 1));
  44.125  by (fast_tac FOL_cs 1);
  44.126  result();
  44.127 @@ -490,8 +490,8 @@
  44.128  
  44.129  writeln"Problem 62 as corrected in AAR newletter #31";
  44.130  goal FOL.thy
  44.131 -    "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->	\
  44.132 -\    (ALL x. (~p(a) | p(x) | p(f(f(x)))) &			\
  44.133 +    "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->     \
  44.134 +\    (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                      \
  44.135  \            (~p(a) | ~p(f(x)) | p(f(f(x)))))";
  44.136  by (fast_tac FOL_cs 1);
  44.137  result();
    45.1 --- a/src/FOL/ex/foundn.ML	Mon Jan 29 13:56:41 1996 +0100
    45.2 +++ b/src/FOL/ex/foundn.ML	Mon Jan 29 13:58:15 1996 +0100
    45.3 @@ -1,6 +1,6 @@
    45.4 -(*  Title: 	FOL/ex/foundn
    45.5 +(*  Title:      FOL/ex/foundn
    45.6      ID:         $Id$
    45.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    45.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    45.9      Copyright   1991  University of Cambridge
   45.10  
   45.11  Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
   45.12 @@ -9,11 +9,11 @@
   45.13  writeln"File FOL/ex/foundn.";
   45.14  
   45.15  goal IFOL.thy "A&B  --> (C-->A&C)";
   45.16 -by (resolve_tac [impI] 1);
   45.17 -by (resolve_tac [impI] 1);
   45.18 -by (resolve_tac [conjI] 1);
   45.19 +by (rtac impI 1);
   45.20 +by (rtac impI 1);
   45.21 +by (rtac conjI 1);
   45.22  by (assume_tac 2);
   45.23 -by (resolve_tac [conjunct1] 1);
   45.24 +by (rtac conjunct1 1);
   45.25  by (assume_tac 1);
   45.26  result();
   45.27  
   45.28 @@ -21,9 +21,9 @@
   45.29  val prems = 
   45.30  goal IFOL.thy "A&B ==> ([| A;  B |] ==> C) ==> C";
   45.31  by (resolve_tac prems 1);
   45.32 -by (resolve_tac [conjunct1] 1);
   45.33 +by (rtac conjunct1 1);
   45.34  by (resolve_tac prems 1);
   45.35 -by (resolve_tac [conjunct2] 1);
   45.36 +by (rtac conjunct2 1);
   45.37  by (resolve_tac prems 1);
   45.38  result();
   45.39  
   45.40 @@ -31,17 +31,17 @@
   45.41  val prems = 
   45.42  goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B";
   45.43  by (resolve_tac prems 1);
   45.44 -by (resolve_tac [notI] 1);
   45.45 +by (rtac notI 1);
   45.46  by (res_inst_tac [ ("P", "~B") ]  notE  1);
   45.47 -by (resolve_tac [notI] 2);
   45.48 +by (rtac notI 2);
   45.49  by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
   45.50  by (assume_tac 2);
   45.51 -by (resolve_tac [disjI1] 2);
   45.52 +by (rtac disjI1 2);
   45.53  by (assume_tac 2);
   45.54 -by (resolve_tac [notI] 1);
   45.55 +by (rtac notI 1);
   45.56  by (res_inst_tac [ ("P", "B | ~B") ]  notE  1);
   45.57  by (assume_tac 1);
   45.58 -by (resolve_tac [disjI2] 1);
   45.59 +by (rtac disjI2 1);
   45.60  by (assume_tac 1);
   45.61  result();
   45.62  
   45.63 @@ -49,23 +49,23 @@
   45.64  val prems = 
   45.65  goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B";
   45.66  by (resolve_tac prems 1);
   45.67 -by (resolve_tac [notI] 1);
   45.68 -by (resolve_tac [notE] 1);
   45.69 -by (resolve_tac [notI] 2);
   45.70 -by (eresolve_tac [notE] 2);
   45.71 -by (eresolve_tac [disjI1] 2);
   45.72 -by (resolve_tac [notI] 1);
   45.73 -by (eresolve_tac [notE] 1);
   45.74 -by (eresolve_tac [disjI2] 1);
   45.75 +by (rtac notI 1);
   45.76 +by (rtac notE 1);
   45.77 +by (rtac notI 2);
   45.78 +by (etac notE 2);
   45.79 +by (etac disjI1 2);
   45.80 +by (rtac notI 1);
   45.81 +by (etac notE 1);
   45.82 +by (etac disjI2 1);
   45.83  result();
   45.84  
   45.85  
   45.86  val prems = 
   45.87  goal IFOL.thy "[| A | ~A;  ~ ~A |] ==> A";
   45.88 -by (resolve_tac [disjE] 1);
   45.89 +by (rtac disjE 1);
   45.90  by (resolve_tac prems 1);
   45.91  by (assume_tac 1);
   45.92 -by (resolve_tac [FalseE] 1);
   45.93 +by (rtac FalseE 1);
   45.94  by (res_inst_tac [ ("P", "~A") ]  notE  1);
   45.95  by (resolve_tac prems 1);
   45.96  by (assume_tac 1);
   45.97 @@ -76,25 +76,25 @@
   45.98  
   45.99  val prems =
  45.100  goal IFOL.thy "ALL z. G(z) ==> ALL z. G(z)|H(z)";
  45.101 -by (resolve_tac [allI] 1);
  45.102 -by (resolve_tac [disjI1] 1);
  45.103 +by (rtac allI 1);
  45.104 +by (rtac disjI1 1);
  45.105  by (resolve_tac (prems RL [spec]) 1); 
  45.106    (*can use instead
  45.107 -    by (resolve_tac [spec] 1);  by (resolve_tac prems 1); *)
  45.108 +    by (rtac spec 1);  by (resolve_tac prems 1); *)
  45.109  result();
  45.110  
  45.111  
  45.112  goal IFOL.thy "ALL x. EX y. x=y";
  45.113 -by (resolve_tac [allI] 1);
  45.114 -by (resolve_tac [exI] 1);
  45.115 -by (resolve_tac [refl] 1);
  45.116 +by (rtac allI 1);
  45.117 +by (rtac exI 1);
  45.118 +by (rtac refl 1);
  45.119  result();
  45.120  
  45.121  
  45.122  goal IFOL.thy "EX y. ALL x. x=y";
  45.123 -by (resolve_tac [exI] 1);
  45.124 -by (resolve_tac [allI] 1);
  45.125 -by (resolve_tac [refl] 1) handle ERROR => writeln"Failed, as expected";  
  45.126 +by (rtac exI 1);
  45.127 +by (rtac allI 1);
  45.128 +by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
  45.129  getgoal 1; 
  45.130  
  45.131  
  45.132 @@ -109,12 +109,12 @@
  45.133  
  45.134  val prems =
  45.135  goal IFOL.thy "(EX z.F(z)) & B ==> (EX z. F(z) & B)";
  45.136 -by (resolve_tac [conjE] 1);
  45.137 +by (rtac conjE 1);
  45.138  by (resolve_tac prems 1);
  45.139 -by (resolve_tac [exE] 1);
  45.140 +by (rtac exE 1);
  45.141  by (assume_tac 1);
  45.142 -by (resolve_tac [exI] 1);
  45.143 -by (resolve_tac [conjI] 1);
  45.144 +by (rtac exI 1);
  45.145 +by (rtac conjI 1);
  45.146  by (assume_tac 1);
  45.147  by (assume_tac 1);
  45.148  result();
  45.149 @@ -122,11 +122,11 @@
  45.150  
  45.151  (*A bigger demonstration of quantifiers -- not in the paper*)
  45.152  goal IFOL.thy "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
  45.153 -by (resolve_tac [impI] 1);
  45.154 -by (resolve_tac [allI] 1);
  45.155 -by (resolve_tac [exE] 1 THEN assume_tac 1);
  45.156 -by (resolve_tac [exI] 1);
  45.157 -by (resolve_tac [allE] 1 THEN assume_tac 1);
  45.158 +by (rtac impI 1);
  45.159 +by (rtac allI 1);
  45.160 +by (rtac exE 1 THEN assume_tac 1);
  45.161 +by (rtac exI 1);
  45.162 +by (rtac allE 1 THEN assume_tac 1);
  45.163  by (assume_tac 1);
  45.164  result();  
  45.165  
    46.1 --- a/src/FOL/ex/int.ML	Mon Jan 29 13:56:41 1996 +0100
    46.2 +++ b/src/FOL/ex/int.ML	Mon Jan 29 13:58:15 1996 +0100
    46.3 @@ -1,6 +1,6 @@
    46.4 -(*  Title: 	FOL/ex/int
    46.5 +(*  Title:      FOL/ex/int
    46.6      ID:         $Id$
    46.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    46.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    46.9      Copyright   1991  University of Cambridge
   46.10  
   46.11  Intuitionistic First-Order Logic
   46.12 @@ -289,8 +289,8 @@
   46.13  result();
   46.14  
   46.15  writeln"Problem ~~26";
   46.16 -goal IFOL.thy "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) &	\
   46.17 -\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))	\
   46.18 +goal IFOL.thy "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) &    \
   46.19 +\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
   46.20  \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
   46.21  (*NOT PROVED*)
   46.22  
   46.23 @@ -378,9 +378,9 @@
   46.24  result();
   46.25  
   46.26  writeln"Problem 44";
   46.27 -goal IFOL.thy "(ALL x. f(x) -->					\
   46.28 -\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &   	\
   46.29 -\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))			\
   46.30 +goal IFOL.thy "(ALL x. f(x) -->                                 \
   46.31 +\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
   46.32 +\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
   46.33  \             --> (EX x. j(x) & ~f(x))";
   46.34  by (Int.fast_tac 1);
   46.35  result();
    47.1 --- a/src/FOL/ex/intro.ML	Mon Jan 29 13:56:41 1996 +0100
    47.2 +++ b/src/FOL/ex/intro.ML	Mon Jan 29 13:58:15 1996 +0100
    47.3 @@ -1,6 +1,6 @@
    47.4 -(*  Title: 	FOL/ex/intro
    47.5 +(*  Title:      FOL/ex/intro
    47.6      ID:         $Id$
    47.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    47.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    47.9      Copyright   1992  University of Cambridge
   47.10  
   47.11  Examples for the manual "Introduction to Isabelle"
   47.12 @@ -15,29 +15,29 @@
   47.13  (**** Some simple backward proofs ****)
   47.14  
   47.15  goal FOL.thy "P|P --> P";
   47.16 -by (resolve_tac [impI] 1);
   47.17 -by (resolve_tac [disjE] 1);
   47.18 +by (rtac impI 1);
   47.19 +by (rtac disjE 1);
   47.20  by (assume_tac 3);
   47.21  by (assume_tac 2);
   47.22  by (assume_tac 1);
   47.23  qed "mythm";
   47.24  
   47.25  goal FOL.thy "(P & Q) | R  --> (P | R)";
   47.26 -by (resolve_tac [impI] 1);
   47.27 -by (eresolve_tac [disjE] 1);
   47.28 -by (dresolve_tac [conjunct1] 1);
   47.29 -by (resolve_tac [disjI1] 1);
   47.30 -by (resolve_tac [disjI2] 2);
   47.31 +by (rtac impI 1);
   47.32 +by (etac disjE 1);
   47.33 +by (dtac conjunct1 1);
   47.34 +by (rtac disjI1 1);
   47.35 +by (rtac disjI2 2);
   47.36  by (REPEAT (assume_tac 1));
   47.37  result();
   47.38  
   47.39  (*Correct version, delaying use of "spec" until last*)
   47.40  goal FOL.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
   47.41 -by (resolve_tac [impI] 1);
   47.42 -by (resolve_tac [allI] 1);
   47.43 -by (resolve_tac [allI] 1);
   47.44 -by (dresolve_tac [spec] 1);
   47.45 -by (dresolve_tac [spec] 1);
   47.46 +by (rtac impI 1);
   47.47 +by (rtac allI 1);
   47.48 +by (rtac allI 1);
   47.49 +by (dtac spec 1);
   47.50 +by (dtac spec 1);
   47.51  by (assume_tac 1);
   47.52  result();
   47.53  
   47.54 @@ -58,7 +58,7 @@
   47.55  (**** Derivation of conjunction elimination rule ****)
   47.56  
   47.57  val [major,minor] = goal FOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R";
   47.58 -by (resolve_tac [minor] 1);
   47.59 +by (rtac minor 1);
   47.60  by (resolve_tac [major RS conjunct1] 1);
   47.61  by (resolve_tac [major RS conjunct2] 1);
   47.62  prth (topthm());
   47.63 @@ -70,17 +70,17 @@
   47.64  (** Derivation of negation introduction **)
   47.65  
   47.66  val prems = goal FOL.thy "(P ==> False) ==> ~P";
   47.67 -by (rewrite_goals_tac [not_def]);
   47.68 -by (resolve_tac [impI] 1);
   47.69 +by (rewtac not_def);
   47.70 +by (rtac impI 1);
   47.71  by (resolve_tac prems 1);
   47.72  by (assume_tac 1);
   47.73  result();
   47.74  
   47.75  val [major,minor] = goal FOL.thy "[| ~P;  P |] ==> R";
   47.76 -by (resolve_tac [FalseE] 1);
   47.77 -by (resolve_tac [mp] 1);
   47.78 +by (rtac FalseE 1);
   47.79 +by (rtac mp 1);
   47.80  by (resolve_tac [rewrite_rule [not_def] major] 1);
   47.81 -by (resolve_tac [minor] 1);
   47.82 +by (rtac minor 1);
   47.83  result();
   47.84  
   47.85  (*Alternative proof of above result*)
    48.1 --- a/src/FOL/ex/mini.ML	Mon Jan 29 13:56:41 1996 +0100
    48.2 +++ b/src/FOL/ex/mini.ML	Mon Jan 29 13:58:15 1996 +0100
    48.3 @@ -1,6 +1,6 @@
    48.4 -(*  Title: 	FOL/ex/mini
    48.5 +(*  Title:      FOL/ex/mini
    48.6      ID:         $Id$
    48.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    48.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    48.9      Copyright   1994  University of Cambridge
   48.10  
   48.11  Classical First-Order Logic
   48.12 @@ -20,52 +20,52 @@
   48.13   (writeln s;  
   48.14    prove_goal FOL.thy s
   48.15     (fn prems => [ (cut_facts_tac prems 1), 
   48.16 -		  (Cla.fast_tac FOL_cs 1) ]));
   48.17 +                  (Cla.fast_tac FOL_cs 1) ]));
   48.18  
   48.19  val demorgans = map prove_fun
   48.20 -    		  ["~(P&Q) <-> ~P | ~Q",
   48.21 -		   "~(P|Q) <-> ~P & ~Q",
   48.22 -		   "~~P <-> P",
   48.23 -		   "~(ALL x.P(x)) <-> (EX x. ~P(x))",
   48.24 -		   "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
   48.25 +                  ["~(P&Q) <-> ~P | ~Q",
   48.26 +                   "~(P|Q) <-> ~P & ~Q",
   48.27 +                   "~~P <-> P",
   48.28 +                   "~(ALL x.P(x)) <-> (EX x. ~P(x))",
   48.29 +                   "~(EX x.P(x)) <-> (ALL x. ~P(x))"];
   48.30  
   48.31  (*** Removal of --> and <-> (positive and negative occurrences) ***)
   48.32  (*Last one is important for computing a compact CNF*)
   48.33  val nnf_rews = map prove_fun
   48.34 -		["(P-->Q) <-> (~P | Q)",
   48.35 -		 "~(P-->Q) <-> (P & ~Q)",
   48.36 -		 "(P<->Q) <-> (~P | Q) & (~Q | P)",
   48.37 -		 "~(P<->Q) <-> (P | Q) & (~P | ~Q)"];
   48.38 +                ["(P-->Q) <-> (~P | Q)",
   48.39 +                 "~(P-->Q) <-> (P & ~Q)",
   48.40 +                 "(P<->Q) <-> (~P | Q) & (~Q | P)",
   48.41 +                 "~(P<->Q) <-> (P | Q) & (~P | ~Q)"];
   48.42  
   48.43  (* BEWARE: rewrite rules for <-> can confuse the simplifier!! *)
   48.44  
   48.45  (*** Pushing in the existential quantifiers ***)
   48.46  
   48.47  val ex_rews = map prove_fun 
   48.48 -		["(EX x. P) <-> P",
   48.49 -		 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
   48.50 -		 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
   48.51 -		 "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
   48.52 -		 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
   48.53 -		 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
   48.54 +                ["(EX x. P) <-> P",
   48.55 +                 "(EX x. P(x) & Q) <-> (EX x.P(x)) & Q",
   48.56 +                 "(EX x. P & Q(x)) <-> P & (EX x.Q(x))",
   48.57 +                 "(EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))",
   48.58 +                 "(EX x. P(x) | Q) <-> (EX x.P(x)) | Q",
   48.59 +                 "(EX x. P | Q(x)) <-> P | (EX x.Q(x))"];
   48.60  
   48.61  (*** Pushing in the universal quantifiers ***)
   48.62  
   48.63  val all_rews = map prove_fun
   48.64 -		["(ALL x. P) <-> P",
   48.65 -		 "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))",
   48.66 -		 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
   48.67 -		 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
   48.68 -		 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
   48.69 -		 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
   48.70 +                ["(ALL x. P) <-> P",
   48.71 +                 "(ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))",
   48.72 +                 "(ALL x. P(x) & Q) <-> (ALL x.P(x)) & Q",
   48.73 +                 "(ALL x. P & Q(x)) <-> P & (ALL x.Q(x))",
   48.74 +                 "(ALL x. P(x) | Q) <-> (ALL x.P(x)) | Q",
   48.75 +                 "(ALL x. P | Q(x)) <-> P | (ALL x.Q(x))"];
   48.76  
   48.77  
   48.78  val mini_ss = 
   48.79    empty_ss 
   48.80    setmksimps (map mk_meta_eq o atomize o gen_all)
   48.81    setsolver  (fn prems => resolve_tac (triv_rls@prems) 
   48.82 -	                  ORELSE' assume_tac
   48.83 -	                  ORELSE' etac FalseE)
   48.84 +                          ORELSE' assume_tac
   48.85 +                          ORELSE' etac FalseE)
   48.86    setsubgoaler asm_simp_tac
   48.87    addsimps (demorgans @ nnf_rews @ ex_rews @ all_rews);
   48.88  
    49.1 --- a/src/FOL/ex/prop.ML	Mon Jan 29 13:56:41 1996 +0100
    49.2 +++ b/src/FOL/ex/prop.ML	Mon Jan 29 13:58:15 1996 +0100
    49.3 @@ -1,6 +1,6 @@
    49.4 -(*  Title: 	FOL/ex/prop
    49.5 +(*  Title:      FOL/ex/prop
    49.6      ID:         $Id$
    49.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    49.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    49.9      Copyright   1991  University of Cambridge
   49.10  
   49.11  First-Order Logic: propositional examples (intuitionistic and classical)
   49.12 @@ -107,13 +107,13 @@
   49.13  
   49.14  (* stab-to-peirce *)
   49.15  goal thy "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
   49.16 -\	      --> ((P --> Q) --> P) --> P";
   49.17 +\             --> ((P --> Q) --> P) --> P";
   49.18  by tac;
   49.19  result();
   49.20  
   49.21  (* peirce-imp1 *)
   49.22  goal thy "(((Q --> R) --> Q) --> Q) \
   49.23 -\	       --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
   49.24 +\              --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
   49.25  by tac;
   49.26  result();
   49.27    
   49.28 @@ -134,10 +134,10 @@
   49.29  
   49.30  (* tatsuta *)
   49.31  goal thy "(((P7 --> P1) --> P10) --> P4 --> P5) \
   49.32 -\	  --> (((P8 --> P2) --> P9) --> P3 --> P10) \
   49.33 -\	  --> (P1 --> P8) --> P6 --> P7 \
   49.34 -\	  --> (((P3 --> P2) --> P9) --> P4) \
   49.35 -\	  --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
   49.36 +\         --> (((P8 --> P2) --> P9) --> P3 --> P10) \
   49.37 +\         --> (P1 --> P8) --> P6 --> P7 \
   49.38 +\         --> (((P3 --> P2) --> P9) --> P4) \
   49.39 +\         --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
   49.40  by tac;
   49.41  result();
   49.42  
    50.1 --- a/src/FOL/ex/quant.ML	Mon Jan 29 13:56:41 1996 +0100
    50.2 +++ b/src/FOL/ex/quant.ML	Mon Jan 29 13:58:15 1996 +0100
    50.3 @@ -1,6 +1,6 @@
    50.4 -(*  Title: 	FOL/ex/quant
    50.5 +(*  Title:      FOL/ex/quant
    50.6      ID:         $Id$
    50.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    50.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    50.9      Copyright   1991  University of Cambridge
   50.10  
   50.11  First-Order Logic: quantifier examples (intuitionistic and classical)
    51.1 --- a/src/FOL/intprover.ML	Mon Jan 29 13:56:41 1996 +0100
    51.2 +++ b/src/FOL/intprover.ML	Mon Jan 29 13:58:15 1996 +0100
    51.3 @@ -1,6 +1,6 @@
    51.4 -(*  Title: 	FOL/int-prover
    51.5 +(*  Title:      FOL/int-prover
    51.6      ID:         $Id$
    51.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    51.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    51.9      Copyright   1992  University of Cambridge
   51.10  
   51.11  A naive prover for intuitionistic logic
   51.12 @@ -56,10 +56,10 @@
   51.13  
   51.14  (*Attack subgoals using safe inferences -- matching, not resolution*)
   51.15  val safe_step_tac = FIRST' [eq_assume_tac,
   51.16 -			    eq_mp_tac,
   51.17 -			    bimatch_tac safe0_brls,
   51.18 -			    hyp_subst_tac,
   51.19 -			    bimatch_tac safep_brls] ;
   51.20 +                            eq_mp_tac,
   51.21 +                            bimatch_tac safe0_brls,
   51.22 +                            hyp_subst_tac,
   51.23 +                            bimatch_tac safep_brls] ;
   51.24  
   51.25  (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   51.26  val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;
    52.1 --- a/src/FOL/simpdata.ML	Mon Jan 29 13:56:41 1996 +0100
    52.2 +++ b/src/FOL/simpdata.ML	Mon Jan 29 13:58:15 1996 +0100
    52.3 @@ -1,6 +1,6 @@
    52.4 -(*  Title: 	FOL/simpdata
    52.5 +(*  Title:      FOL/simpdata
    52.6      ID:         $Id$
    52.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    52.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    52.9      Copyright   1994  University of Cambridge
   52.10  
   52.11  Simplification data for FOL
   52.12 @@ -12,37 +12,37 @@
   52.13   (writeln s;  
   52.14    prove_goal IFOL.thy s
   52.15     (fn prems => [ (cut_facts_tac prems 1), 
   52.16 -		  (Int.fast_tac 1) ]));
   52.17 +                  (Int.fast_tac 1) ]));
   52.18  
   52.19  val conj_rews = map int_prove_fun
   52.20 - ["P & True <-> P", 	 "True & P <-> P",
   52.21 + ["P & True <-> P",      "True & P <-> P",
   52.22    "P & False <-> False", "False & P <-> False",
   52.23    "P & P <-> P",
   52.24 -  "P & ~P <-> False", 	 "~P & P <-> False",
   52.25 +  "P & ~P <-> False",    "~P & P <-> False",
   52.26    "(P & Q) & R <-> P & (Q & R)"];
   52.27  
   52.28  val disj_rews = map int_prove_fun
   52.29 - ["P | True <-> True", 	"True | P <-> True",
   52.30 -  "P | False <-> P", 	"False | P <-> P",
   52.31 + ["P | True <-> True",  "True | P <-> True",
   52.32 +  "P | False <-> P",    "False | P <-> P",
   52.33    "P | P <-> P",
   52.34    "(P | Q) | R <-> P | (Q | R)"];
   52.35  
   52.36  val not_rews = map int_prove_fun
   52.37   ["~(P|Q)  <-> ~P & ~Q",
   52.38 -  "~ False <-> True",	"~ True <-> False"];
   52.39 +  "~ False <-> True",   "~ True <-> False"];
   52.40  
   52.41  val imp_rews = map int_prove_fun
   52.42 - ["(P --> False) <-> ~P",	"(P --> True) <-> True",
   52.43 -  "(False --> P) <-> True",	"(True --> P) <-> P", 
   52.44 -  "(P --> P) <-> True",		"(P --> ~P) <-> ~P"];
   52.45 + ["(P --> False) <-> ~P",       "(P --> True) <-> True",
   52.46 +  "(False --> P) <-> True",     "(True --> P) <-> P", 
   52.47 +  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
   52.48  
   52.49  val iff_rews = map int_prove_fun
   52.50 - ["(True <-> P) <-> P", 	"(P <-> True) <-> P",
   52.51 + ["(True <-> P) <-> P",         "(P <-> True) <-> P",
   52.52    "(P <-> P) <-> True",
   52.53 -  "(False <-> P) <-> ~P", 	"(P <-> False) <-> ~P"];
   52.54 +  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
   52.55  
   52.56  val quant_rews = map int_prove_fun
   52.57 - ["(ALL x.P) <-> P",	"(EX x.P) <-> P"];
   52.58 + ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
   52.59  
   52.60  (*These are NOT supplied by default!*)
   52.61  val distrib_rews  = map int_prove_fun
   52.62 @@ -62,12 +62,12 @@
   52.63    case concl_of r of
   52.64      Const("Trueprop",_) $ p =>
   52.65        (case p of
   52.66 -	 Const("op -->",_)$_$_ => atomize(r RS mp)
   52.67 +         Const("op -->",_)$_$_ => atomize(r RS mp)
   52.68         | Const("op &",_)$_$_   => atomize(r RS conjunct1) @
   52.69 -	  		          atomize(r RS conjunct2)
   52.70 +                                  atomize(r RS conjunct2)
   52.71         | Const("All",_)$_      => atomize(r RS spec)
   52.72 -       | Const("True",_)       => []	(*True is DELETED*)
   52.73 -       | Const("False",_)      => []	(*should False do something?*)
   52.74 +       | Const("True",_)       => []    (*True is DELETED*)
   52.75 +       | Const("False",_)      => []    (*should False do something?*)
   52.76         | _                     => [r])
   52.77    | _ => [r];
   52.78  
   52.79 @@ -111,8 +111,8 @@
   52.80    empty_ss 
   52.81    setmksimps (map mk_meta_eq o atomize o gen_all)
   52.82    setsolver  (fn prems => resolve_tac (triv_rls@prems) 
   52.83 -	                  ORELSE' assume_tac
   52.84 -	                  ORELSE' etac FalseE)
   52.85 +                          ORELSE' assume_tac
   52.86 +                          ORELSE' etac FalseE)
   52.87    setsubgoaler asm_simp_tac
   52.88    addsimps IFOL_rews
   52.89    addcongs [imp_cong];
   52.90 @@ -122,12 +122,12 @@
   52.91   (writeln s;  
   52.92    prove_goal FOL.thy s
   52.93     (fn prems => [ (cut_facts_tac prems 1), 
   52.94 -		  (Cla.fast_tac FOL_cs 1) ]));
   52.95 +                  (Cla.fast_tac FOL_cs 1) ]));
   52.96  
   52.97  val cla_rews = map prove_fun
   52.98   ["~(P&Q)  <-> ~P | ~Q",
   52.99 -  "P | ~P", 		"~P | P",
  52.100 -  "~ ~ P <-> P",	"(~P --> P) <-> P"];
  52.101 +  "P | ~P",             "~P | P",
  52.102 +  "~ ~ P <-> P",        "(~P --> P) <-> P"];
  52.103  
  52.104  val FOL_ss = IFOL_ss addsimps cla_rews;
  52.105  
    53.1 --- a/src/FOLP/FOLP.ML	Mon Jan 29 13:56:41 1996 +0100
    53.2 +++ b/src/FOLP/FOLP.ML	Mon Jan 29 13:58:15 1996 +0100
    53.3 @@ -1,6 +1,6 @@
    53.4 -(*  Title: 	FOLP/FOLP.ML
    53.5 +(*  Title:      FOLP/FOLP.ML
    53.6      ID:         $Id$
    53.7 -    Author: 	Martin D Coen, Cambridge University Computer Laboratory
    53.8 +    Author:     Martin D Coen, Cambridge University Computer Laboratory
    53.9      Copyright   1991  University of Cambridge
   53.10  
   53.11  Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
   53.12 @@ -29,7 +29,7 @@
   53.13  val disjCI = prove_goal FOLP.thy 
   53.14     "(!!x.x:~Q ==> f(x):P) ==> ?p : P|Q"
   53.15   (fn prems=>
   53.16 -  [ (resolve_tac [classical] 1),
   53.17 +  [ (rtac classical 1),
   53.18      (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
   53.19      (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
   53.20  
   53.21 @@ -37,17 +37,17 @@
   53.22  val ex_classical = prove_goal FOLP.thy 
   53.23     "( !!u.u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
   53.24   (fn prems=>
   53.25 -  [ (resolve_tac [classical] 1),
   53.26 +  [ (rtac classical 1),
   53.27      (eresolve_tac (prems RL [exI]) 1) ]);
   53.28  
   53.29  (*version of above, simplifying ~EX to ALL~ *)
   53.30  val exCI = prove_goal FOLP.thy 
   53.31     "(!!u.u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x.P(x)"
   53.32   (fn [prem]=>
   53.33 -  [ (resolve_tac [ex_classical] 1),
   53.34 +  [ (rtac ex_classical 1),
   53.35      (resolve_tac [notI RS allI RS prem] 1),
   53.36 -    (eresolve_tac [notE] 1),
   53.37 -    (eresolve_tac [exI] 1) ]);
   53.38 +    (etac notE 1),
   53.39 +    (etac exI 1) ]);
   53.40  
   53.41  val excluded_middle = prove_goal FOLP.thy "?p : ~P | P"
   53.42   (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
   53.43 @@ -66,7 +66,7 @@
   53.44  (*Double negation law*)
   53.45  val notnotD = prove_goal FOLP.thy "p:~~P ==> ?p : P"
   53.46   (fn [major]=>
   53.47 -  [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
   53.48 +  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
   53.49  
   53.50  
   53.51  (*** Tactics for implication and contradiction ***)
   53.52 @@ -77,16 +77,16 @@
   53.53      "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
   53.54  \                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R"
   53.55   (fn prems =>
   53.56 -  [ (resolve_tac [conjE] 1),
   53.57 +  [ (rtac conjE 1),
   53.58      (REPEAT (DEPTH_SOLVE_1 
   53.59 -	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
   53.60 +        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
   53.61  
   53.62  
   53.63  (*Should be used as swap since ~P becomes redundant*)
   53.64  val swap = prove_goal FOLP.thy 
   53.65     "p:~P ==> (!!x.x:~Q ==> f(x):P) ==> ?p : Q"
   53.66   (fn major::prems=>
   53.67 -  [ (resolve_tac [classical] 1),
   53.68 +  [ (rtac classical 1),
   53.69      (rtac (major RS notE) 1),
   53.70      (REPEAT (ares_tac prems 1)) ]);
   53.71  
    54.1 --- a/src/FOLP/IFOLP.ML	Mon Jan 29 13:56:41 1996 +0100
    54.2 +++ b/src/FOLP/IFOLP.ML	Mon Jan 29 13:58:15 1996 +0100
    54.3 @@ -1,6 +1,6 @@
    54.4 -(*  Title: 	FOLP/IFOLP.ML
    54.5 +(*  Title:      FOLP/IFOLP.ML
    54.6      ID:         $Id$
    54.7 -    Author: 	Martin D Coen, Cambridge University Computer Laboratory
    54.8 +    Author:     Martin D Coen, Cambridge University Computer Laboratory
    54.9      Copyright   1992  University of Cambridge
   54.10  
   54.11  Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
   54.12 @@ -140,9 +140,9 @@
   54.13        let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
   54.14            and concl = discard_proof (Logic.strip_assums_concl prem)
   54.15        in  
   54.16 -	  if exists (fn hyp => hyp aconv concl) hyps
   54.17 -	  then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of
   54.18 -	           [_] => assume_tac i
   54.19 +          if exists (fn hyp => hyp aconv concl) hyps
   54.20 +          then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of
   54.21 +                   [_] => assume_tac i
   54.22                   |  _  => no_tac
   54.23            else no_tac
   54.24        end);
   54.25 @@ -168,7 +168,7 @@
   54.26  (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   54.27  val iffE = prove_goalw IFOLP.thy [iff_def]
   54.28      "[| p:P <-> Q;  !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R"
   54.29 - (fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]);
   54.30 + (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);
   54.31  
   54.32  (* Destruct rules for <-> similar to Modus Ponens *)
   54.33  
   54.34 @@ -241,14 +241,14 @@
   54.35   (fn prems =>
   54.36    [ (cut_facts_tac prems 1),
   54.37      (REPEAT   (ares_tac [iffI,impI] 1
   54.38 -      ORELSE  eresolve_tac [iffE] 1
   54.39 +      ORELSE  etac iffE 1
   54.40        ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
   54.41  
   54.42  val iff_cong = prove_goal IFOLP.thy 
   54.43      "[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
   54.44   (fn prems =>
   54.45    [ (cut_facts_tac prems 1),
   54.46 -    (REPEAT   (eresolve_tac [iffE] 1
   54.47 +    (REPEAT   (etac iffE 1
   54.48        ORELSE  ares_tac [iffI] 1
   54.49        ORELSE  mp_tac 1)) ]);
   54.50  
   54.51 @@ -265,12 +265,12 @@
   54.52   (fn prems =>
   54.53    [ (REPEAT   (ares_tac [iffI,allI] 1
   54.54        ORELSE   mp_tac 1
   54.55 -      ORELSE   eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]);
   54.56 +      ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
   54.57  
   54.58  val ex_cong = prove_goal IFOLP.thy 
   54.59      "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX x.P(x)) <-> (EX x.Q(x))"
   54.60   (fn prems =>
   54.61 -  [ (REPEAT   (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1
   54.62 +  [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   54.63        ORELSE   mp_tac 1
   54.64        ORELSE   iff_tac prems 1)) ]);
   54.65  
   54.66 @@ -320,7 +320,7 @@
   54.67     "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
   54.68   (fn prems=>
   54.69    [ (resolve_tac (prems RL [ssubst]) 1),
   54.70 -    (resolve_tac [refl] 1) ]);
   54.71 +    (rtac refl 1) ]);
   54.72  
   54.73  val subst_context2 = prove_goal IFOLP.thy 
   54.74     "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
   54.75 @@ -333,23 +333,23 @@
   54.76    [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   54.77  
   54.78  (*Useful with eresolve_tac for proving equalties from known equalities.
   54.79 -	a = b
   54.80 -	|   |
   54.81 -	c = d	*)
   54.82 +        a = b
   54.83 +        |   |
   54.84 +        c = d   *)
   54.85  val box_equals = prove_goal IFOLP.thy
   54.86      "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"  
   54.87   (fn prems=>
   54.88 -  [ (resolve_tac [trans] 1),
   54.89 -    (resolve_tac [trans] 1),
   54.90 -    (resolve_tac [sym] 1),
   54.91 +  [ (rtac trans 1),
   54.92 +    (rtac trans 1),
   54.93 +    (rtac sym 1),
   54.94      (REPEAT (resolve_tac prems 1)) ]);
   54.95  
   54.96  (*Dual of box_equals: for proving equalities backwards*)
   54.97  val simp_equals = prove_goal IFOLP.thy
   54.98      "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"  
   54.99   (fn prems=>
  54.100 -  [ (resolve_tac [trans] 1),
  54.101 -    (resolve_tac [trans] 1),
  54.102 +  [ (rtac trans 1),
  54.103 +    (rtac trans 1),
  54.104      (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]);
  54.105  
  54.106  (** Congruence rules for predicate letters **)
  54.107 @@ -379,9 +379,9 @@
  54.108  
  54.109  val pred_congs = 
  54.110      flat (map (fn c => 
  54.111 -	       map (fn th => read_instantiate [("P",c)] th)
  54.112 -		   [pred1_cong,pred2_cong,pred3_cong])
  54.113 -	       (explode"PQRS"));
  54.114 +               map (fn th => read_instantiate [("P",c)] th)
  54.115 +                   [pred1_cong,pred2_cong,pred3_cong])
  54.116 +               (explode"PQRS"));
  54.117  
  54.118  (*special case for the equality predicate!*)
  54.119  val eq_cong = read_instantiate [("P","op =")] pred2_cong;
    55.1 --- a/src/FOLP/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
    55.2 +++ b/src/FOLP/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
    55.3 @@ -1,6 +1,6 @@
    55.4 -(*  Title: 	FOLP/ROOT
    55.5 +(*  Title:      FOLP/ROOT
    55.6      ID:         $Id$
    55.7 -    Author: 	martin Coen, Cambridge University Computer Laboratory
    55.8 +    Author:     martin Coen, Cambridge University Computer Laboratory
    55.9      Copyright   1993  University of Cambridge
   55.10  
   55.11  Modifed version of Lawrence Paulson's FOL that contains proof terms.
   55.12 @@ -20,7 +20,7 @@
   55.13  
   55.14  use "hypsubst.ML";
   55.15  use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
   55.16 -use "simp.ML";	         (* Patched 'cos matching won't instantiate proof *)
   55.17 +use "simp.ML";           (* Patched 'cos matching won't instantiate proof *)
   55.18  
   55.19  
   55.20  (*** Applying HypsubstFun to generate hyp_subst_tac ***)
   55.21 @@ -34,7 +34,7 @@
   55.22  
   55.23    (*etac rev_cut_eq moves an equality to be the last premise. *)
   55.24    val rev_cut_eq = prove_goal IFOLP.thy 
   55.25 -		"[| p:a=b;  !!x.x:a=b ==> f(x):R |] ==> ?p:R"
   55.26 +                "[| p:a=b;  !!x.x:a=b ==> f(x):R |] ==> ?p:R"
   55.27     (fn prems => [ REPEAT(resolve_tac prems 1) ]);
   55.28  
   55.29    val rev_mp = rev_mp
   55.30 @@ -78,4 +78,4 @@
   55.31  use "../Pure/install_pp.ML";
   55.32  print_depth 8;
   55.33  
   55.34 -val FOLP_build_completed = ();	(*indicate successful build*)
   55.35 +val FOLP_build_completed = ();  (*indicate successful build*)
    56.1 --- a/src/FOLP/classical.ML	Mon Jan 29 13:56:41 1996 +0100
    56.2 +++ b/src/FOLP/classical.ML	Mon Jan 29 13:58:15 1996 +0100
    56.3 @@ -1,6 +1,6 @@
    56.4 -(*  Title: 	FOLP/classical
    56.5 +(*  Title:      FOLP/classical
    56.6      ID:         $Id$
    56.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    56.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    56.9      Copyright   1992  University of Cambridge
   56.10  
   56.11  Like Provers/classical but modified because match_tac is unsuitable for
   56.12 @@ -19,10 +19,10 @@
   56.13  
   56.14  signature CLASSICAL_DATA =
   56.15    sig
   56.16 -  val mp: thm    		(* [| P-->Q;  P |] ==> Q *)
   56.17 -  val not_elim: thm		(* [| ~P;  P |] ==> R *)
   56.18 -  val swap: thm			(* ~P ==> (~Q ==> P) ==> Q *)
   56.19 -  val sizef : thm -> int	(* size function for BEST_FIRST *)
   56.20 +  val mp: thm                   (* [| P-->Q;  P |] ==> Q *)
   56.21 +  val not_elim: thm             (* [| ~P;  P |] ==> R *)
   56.22 +  val swap: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
   56.23 +  val sizef : thm -> int        (* size function for BEST_FIRST *)
   56.24    val hyp_subst_tacs: (int -> tactic) list
   56.25    end;
   56.26  
   56.27 @@ -71,7 +71,7 @@
   56.28  val imp_elim = make_elim mp;
   56.29  
   56.30  (*Solve goal that assumes both P and ~P. *)
   56.31 -val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
   56.32 +val contr_tac = etac not_elim THEN'  assume_tac;
   56.33  
   56.34  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   56.35  fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
   56.36 @@ -94,13 +94,13 @@
   56.37  
   56.38  datatype claset =
   56.39   CS of {safeIs: thm list,
   56.40 -	safeEs: thm list,
   56.41 -	hazIs: thm list,
   56.42 -	hazEs: thm list,
   56.43 -	(*the following are computed from the above*)
   56.44 -	safe0_brls: (bool*thm)list,
   56.45 -	safep_brls: (bool*thm)list,
   56.46 -	haz_brls: (bool*thm)list};
   56.47 +        safeEs: thm list,
   56.48 +        hazIs: thm list,
   56.49 +        hazEs: thm list,
   56.50 +        (*the following are computed from the above*)
   56.51 +        safe0_brls: (bool*thm)list,
   56.52 +        safep_brls: (bool*thm)list,
   56.53 +        haz_brls: (bool*thm)list};
   56.54    
   56.55  fun rep_claset (CS x) = x;
   56.56  
   56.57 @@ -115,8 +115,8 @@
   56.58            partition (apl(0,op=) o subgoals_of_brl) 
   56.59               (sort lessb (joinrules(safeIs, safeEs)))
   56.60    in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
   56.61 -	safe0_brls=safe0_brls, safep_brls=safep_brls,
   56.62 -	haz_brls = sort lessb (joinrules(hazIs, hazEs))}
   56.63 +        safe0_brls=safe0_brls, safep_brls=safep_brls,
   56.64 +        haz_brls = sort lessb (joinrules(hazIs, hazEs))}
   56.65    end;
   56.66  
   56.67  (*** Manipulation of clasets ***)
   56.68 @@ -151,10 +151,10 @@
   56.69  (*Attack subgoals using safe inferences*)
   56.70  fun safe_step_tac (CS{safe0_brls,safep_brls,...}) = 
   56.71    FIRST' [uniq_assume_tac,
   56.72 -	  uniq_mp_tac,
   56.73 -	  biresolve_tac safe0_brls,
   56.74 -	  FIRST' hyp_subst_tacs,
   56.75 -	  biresolve_tac safep_brls] ;
   56.76 +          uniq_mp_tac,
   56.77 +          biresolve_tac safe0_brls,
   56.78 +          FIRST' hyp_subst_tacs,
   56.79 +          biresolve_tac safep_brls] ;
   56.80  
   56.81  (*Repeatedly attack subgoals using safe inferences*)
   56.82  fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));
    57.1 --- a/src/FOLP/ex/If.ML	Mon Jan 29 13:56:41 1996 +0100
    57.2 +++ b/src/FOLP/ex/If.ML	Mon Jan 29 13:58:15 1996 +0100
    57.3 @@ -1,6 +1,6 @@
    57.4 -(*  Title: 	FOLP/ex/if
    57.5 +(*  Title:      FOLP/ex/if
    57.6      ID:         $Id$
    57.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    57.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    57.9      Copyright   1991  University of Cambridge
   57.10  
   57.11  For ex/if.thy.  First-Order Logic: the 'if' example
   57.12 @@ -24,11 +24,11 @@
   57.13  
   57.14  goal If.thy
   57.15      "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
   57.16 -by (resolve_tac [iffI] 1);
   57.17 -by (eresolve_tac [ifE] 1);
   57.18 -by (eresolve_tac [ifE] 1);
   57.19 -by (resolve_tac [ifI] 1);
   57.20 -by (resolve_tac [ifI] 1);
   57.21 +by (rtac iffI 1);
   57.22 +by (etac ifE 1);
   57.23 +by (etac ifE 1);
   57.24 +by (rtac ifI 1);
   57.25 +by (rtac ifI 1);
   57.26  
   57.27  choplev 0;
   57.28  val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE];
    58.1 --- a/src/FOLP/ex/Nat.ML	Mon Jan 29 13:56:41 1996 +0100
    58.2 +++ b/src/FOLP/ex/Nat.ML	Mon Jan 29 13:58:15 1996 +0100
    58.3 @@ -1,6 +1,6 @@
    58.4 -(*  Title: 	FOLP/ex/nat.ML
    58.5 +(*  Title:      FOLP/ex/nat.ML
    58.6      ID:         $Id$
    58.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    58.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    58.9      Copyright   1992  University of Cambridge
   58.10  
   58.11  Examples for the manual "Introduction to Isabelle"
   58.12 @@ -59,7 +59,7 @@
   58.13  
   58.14  
   58.15  val add_ss = FOLP_ss  addcongs nat_congs  
   58.16 -	             addrews  [add_0, add_Suc];
   58.17 +                     addrews  [add_0, add_Suc];
   58.18  
   58.19  goal Nat.thy "?p : (k+m)+n = k+(m+n)";
   58.20  by (res_inst_tac [("n","k")] induct 1);
    59.1 --- a/src/FOLP/ex/Prolog.ML	Mon Jan 29 13:56:41 1996 +0100
    59.2 +++ b/src/FOLP/ex/Prolog.ML	Mon Jan 29 13:58:15 1996 +0100
    59.3 @@ -1,6 +1,6 @@
    59.4 -(*  Title: 	FOL/ex/prolog.ML
    59.5 +(*  Title:      FOL/ex/prolog.ML
    59.6      ID:         $Id$
    59.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    59.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    59.9      Copyright   1992  University of Cambridge
   59.10  
   59.11  For ex/prolog.thy.  First-Order Logic: PROLOG examples
    60.1 --- a/src/FOLP/ex/ROOT.ML	Mon Jan 29 13:56:41 1996 +0100
    60.2 +++ b/src/FOLP/ex/ROOT.ML	Mon Jan 29 13:58:15 1996 +0100
    60.3 @@ -1,6 +1,6 @@
    60.4 -(*  Title: 	FOLP/ex/ROOT
    60.5 +(*  Title:      FOLP/ex/ROOT
    60.6      ID:         $Id$
    60.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    60.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    60.9      Copyright   1992  University of Cambridge
   60.10  
   60.11  Executes all examples for First-Order Logic. 
   60.12 @@ -8,7 +8,7 @@
   60.13  
   60.14  writeln"Root file for FOLP examples";
   60.15  
   60.16 -FOLP_build_completed;	(*Cause examples to fail if FOLP did*)
   60.17 +FOLP_build_completed;   (*Cause examples to fail if FOLP did*)
   60.18  
   60.19  proof_timing := true;
   60.20  
    61.1 --- a/src/FOLP/ex/cla.ML	Mon Jan 29 13:56:41 1996 +0100
    61.2 +++ b/src/FOLP/ex/cla.ML	Mon Jan 29 13:58:15 1996 +0100
    61.3 @@ -1,6 +1,6 @@
    61.4 -(*  Title: 	FOLP/ex/cla
    61.5 +(*  Title:      FOLP/ex/cla
    61.6      ID:         $Id$
    61.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    61.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    61.9      Copyright   1993  University of Cambridge
   61.10  
   61.11  Classical First-Order Logic
   61.12 @@ -207,8 +207,8 @@
   61.13  result();
   61.14  
   61.15  writeln"Problem 26";
   61.16 -goal FOLP.thy "?u : ((EX x. p(x)) <-> (EX x. q(x))) &	\
   61.17 -\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))	\
   61.18 +goal FOLP.thy "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   \
   61.19 +\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
   61.20  \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
   61.21  by (fast_tac FOLP_cs 1);
   61.22  result();
   61.23 @@ -301,15 +301,15 @@
   61.24  result();
   61.25  
   61.26  writeln"Problem 41";
   61.27 -goal FOLP.thy "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))	\
   61.28 +goal FOLP.thy "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))  \
   61.29  \         --> ~ (EX z. ALL x. f(x,z))";
   61.30  by (best_tac FOLP_cs 1);
   61.31  result();
   61.32  
   61.33  writeln"Problem 44";
   61.34 -goal FOLP.thy "?p : (ALL x. f(x) -->					\
   61.35 -\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &   	\
   61.36 -\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))			\
   61.37 +goal FOLP.thy "?p : (ALL x. f(x) -->                                    \
   61.38 +\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
   61.39 +\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
   61.40  \             --> (EX x. j(x) & ~f(x))";
   61.41  by (fast_tac FOLP_cs 1);
   61.42  result();
    62.1 --- a/src/FOLP/ex/foundn.ML	Mon Jan 29 13:56:41 1996 +0100
    62.2 +++ b/src/FOLP/ex/foundn.ML	Mon Jan 29 13:58:15 1996 +0100
    62.3 @@ -1,6 +1,6 @@
    62.4 -(*  Title: 	FOL/ex/foundn
    62.5 +(*  Title:      FOL/ex/foundn
    62.6      ID:         $Id$
    62.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    62.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    62.9      Copyright   1991  University of Cambridge
   62.10  
   62.11  Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
   62.12 @@ -9,11 +9,11 @@
   62.13  writeln"File FOL/ex/foundn.";
   62.14  
   62.15  goal IFOLP.thy "?p : A&B  --> (C-->A&C)";
   62.16 -by (resolve_tac [impI] 1);
   62.17 -by (resolve_tac [impI] 1);
   62.18 -by (resolve_tac [conjI] 1);
   62.19 +by (rtac impI 1);
   62.20 +by (rtac impI 1);
   62.21 +by (rtac conjI 1);
   62.22  by (assume_tac 2);
   62.23 -by (resolve_tac [conjunct1] 1);
   62.24 +by (rtac conjunct1 1);
   62.25  by (assume_tac 1);
   62.26  result();
   62.27  
   62.28 @@ -21,9 +21,9 @@
   62.29  val prems = 
   62.30  goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
   62.31  by (resolve_tac prems 1);
   62.32 -by (resolve_tac [conjunct1] 1);
   62.33 +by (rtac conjunct1 1);
   62.34  by (resolve_tac prems 1);
   62.35 -by (resolve_tac [conjunct2] 1);
   62.36 +by (rtac conjunct2 1);
   62.37  by (resolve_tac prems 1);
   62.38  result();
   62.39  
   62.40 @@ -31,17 +31,17 @@
   62.41  val prems = 
   62.42  goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
   62.43  by (resolve_tac prems 1);
   62.44 -by (resolve_tac [notI] 1);
   62.45 +by (rtac notI 1);
   62.46  by (res_inst_tac [ ("P", "~B") ]  notE  1);
   62.47 -by (resolve_tac [notI] 2);
   62.48 +by (rtac notI 2);
   62.49  by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
   62.50  by (assume_tac 2);
   62.51 -by (resolve_tac [disjI1] 2);
   62.52 +by (rtac disjI1 2);
   62.53  by (assume_tac 2);
   62.54 -by (resolve_tac [notI] 1);
   62.55 +by (rtac notI 1);
   62.56  by (res_inst_tac [ ("P", "B | ~B") ]  notE  1);
   62.57  by (assume_tac 1);
   62.58 -by (resolve_tac [disjI2] 1);
   62.59 +by (rtac disjI2 1);
   62.60  by (assume_tac 1);
   62.61  result();
   62.62  
   62.63 @@ -49,23 +49,23 @@
   62.64  val prems = 
   62.65  goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
   62.66  by (resolve_tac prems 1);
   62.67 -by (resolve_tac [notI] 1);
   62.68 -by (resolve_tac [notE] 1);
   62.69 -by (resolve_tac [notI] 2);
   62.70 -by (eresolve_tac [notE] 2);
   62.71 -by (eresolve_tac [disjI1] 2);
   62.72 -by (resolve_tac [notI] 1);
   62.73 -by (eresolve_tac [notE] 1);
   62.74 -by (eresolve_tac [disjI2] 1);
   62.75 +by (rtac notI 1);
   62.76 +by (rtac notE 1);
   62.77 +by (rtac notI 2);
   62.78 +by (etac notE 2);
   62.79 +by (etac disjI1 2);
   62.80 +by (rtac notI 1);
   62.81 +by (etac notE 1);
   62.82 +by (etac disjI2 1);
   62.83  result();
   62.84  
   62.85  
   62.86  val prems = 
   62.87  goal IFOLP.thy "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
   62.88 -by (resolve_tac [disjE] 1);
   62.89 +by (rtac disjE 1);
   62.90  by (resolve_tac prems 1);
   62.91  by (assume_tac 1);
   62.92 -by (resolve_tac [FalseE] 1);
   62.93 +by (rtac FalseE 1);
   62.94  by (res_inst_tac [ ("P", "~A") ]  notE  1);
   62.95  by (resolve_tac prems 1);
   62.96  by (assume_tac 1);
   62.97 @@ -76,25 +76,25 @@
   62.98  
   62.99  val prems =
  62.100  goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
  62.101 -by (resolve_tac [allI] 1);
  62.102 -by (resolve_tac [disjI1] 1);
  62.103 +by (rtac allI 1);
  62.104 +by (rtac disjI1 1);
  62.105  by (resolve_tac (prems RL [spec]) 1); 
  62.106    (*can use instead
  62.107 -    by (resolve_tac [spec] 1);  by (resolve_tac prems 1); *)
  62.108 +    by (rtac spec 1);  by (resolve_tac prems 1); *)
  62.109  result();
  62.110  
  62.111  
  62.112  goal IFOLP.thy "?p : ALL x. EX y. x=y";
  62.113 -by (resolve_tac [allI] 1);
  62.114 -by (resolve_tac [exI] 1);
  62.115 -by (resolve_tac [refl] 1);
  62.116 +by (rtac allI 1);
  62.117 +by (rtac exI 1);
  62.118 +by (rtac refl 1);
  62.119  result();
  62.120  
  62.121  
  62.122  goal IFOLP.thy "?p : EX y. ALL x. x=y";
  62.123 -by (resolve_tac [exI] 1);
  62.124 -by (resolve_tac [allI] 1);
  62.125 -by (resolve_tac [refl] 1) handle ERROR => writeln"Failed, as expected";  
  62.126 +by (rtac exI 1);
  62.127 +by (rtac allI 1);
  62.128 +by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
  62.129  getgoal 1; 
  62.130  
  62.131  
  62.132 @@ -109,12 +109,12 @@
  62.133  
  62.134  val prems =
  62.135  goal IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";
  62.136 -by (resolve_tac [conjE] 1);
  62.137 +by (rtac conjE 1);
  62.138  by (resolve_tac prems 1);
  62.139 -by (resolve_tac [exE] 1);
  62.140 +by (rtac exE 1);
  62.141  by (assume_tac 1);
  62.142 -by (resolve_tac [exI] 1);
  62.143 -by (resolve_tac [conjI] 1);
  62.144 +by (rtac exI 1);
  62.145 +by (rtac conjI 1);
  62.146  by (assume_tac 1);
  62.147  by (assume_tac 1);
  62.148  result();
  62.149 @@ -122,11 +122,11 @@
  62.150  
  62.151  (*A bigger demonstration of quantifiers -- not in the paper*)
  62.152  goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
  62.153 -by (resolve_tac [impI] 1);
  62.154 -by (resolve_tac [allI] 1);
  62.155 -by (resolve_tac [exE] 1 THEN assume_tac 1);
  62.156 -by (resolve_tac [exI] 1);
  62.157 -by (resolve_tac [allE] 1 THEN assume_tac 1);
  62.158 +by (rtac impI 1);
  62.159 +by (rtac allI 1);
  62.160 +by (rtac exE 1 THEN assume_tac 1);
  62.161 +by (rtac exI 1);
  62.162 +by (rtac allE 1 THEN assume_tac 1);
  62.163  by (assume_tac 1);
  62.164  result();  
  62.165  
    63.1 --- a/src/FOLP/ex/int.ML	Mon Jan 29 13:56:41 1996 +0100
    63.2 +++ b/src/FOLP/ex/int.ML	Mon Jan 29 13:58:15 1996 +0100
    63.3 @@ -1,6 +1,6 @@
    63.4 -(*  Title: 	FOL/ex/int
    63.5 +(*  Title:      FOL/ex/int
    63.6      ID:         $Id$
    63.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    63.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    63.9      Copyright   1991  University of Cambridge
   63.10  
   63.11  Intuitionistic First-Order Logic
   63.12 @@ -320,9 +320,9 @@
   63.13  result();
   63.14  
   63.15  writeln"Problem 44";
   63.16 -goal IFOLP.thy "?p : (ALL x. f(x) -->					\
   63.17 -\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &   	\
   63.18 -\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))			\
   63.19 +goal IFOLP.thy "?p : (ALL x. f(x) -->                                   \
   63.20 +\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
   63.21 +\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
   63.22  \             --> (EX x. j(x) & ~f(x))";
   63.23  by (Int.fast_tac 1);
   63.24  result();
    64.1 --- a/src/FOLP/ex/prop.ML	Mon Jan 29 13:56:41 1996 +0100
    64.2 +++ b/src/FOLP/ex/prop.ML	Mon Jan 29 13:58:15 1996 +0100
    64.3 @@ -1,6 +1,6 @@
    64.4 -(*  Title: 	FOL/ex/prop
    64.5 +(*  Title:      FOL/ex/prop
    64.6      ID:         $Id$
    64.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    64.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    64.9      Copyright   1991  University of Cambridge
   64.10  
   64.11  First-Order Logic: propositional examples (intuitionistic and classical)
   64.12 @@ -107,13 +107,13 @@
   64.13  
   64.14  (* stab-to-peirce *)
   64.15  goal thy "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
   64.16 -\	      --> ((P --> Q) --> P) --> P";
   64.17 +\             --> ((P --> Q) --> P) --> P";
   64.18  by tac;
   64.19  result();
   64.20  
   64.21  (* peirce-imp1 *)
   64.22  goal thy "?p : (((Q --> R) --> Q) --> Q) \
   64.23 -\	       --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
   64.24 +\              --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
   64.25  by tac;
   64.26  result();
   64.27    
   64.28 @@ -134,10 +134,10 @@
   64.29  
   64.30  (* tatsuta *)
   64.31  goal thy "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \
   64.32 -\	  --> (((P8 --> P2) --> P9) --> P3 --> P10) \
   64.33 -\	  --> (P1 --> P8) --> P6 --> P7 \
   64.34 -\	  --> (((P3 --> P2) --> P9) --> P4) \
   64.35 -\	  --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
   64.36 +\         --> (((P8 --> P2) --> P9) --> P3 --> P10) \
   64.37 +\         --> (P1 --> P8) --> P6 --> P7 \
   64.38 +\         --> (((P3 --> P2) --> P9) --> P4) \
   64.39 +\         --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
   64.40  by tac;
   64.41  result();
   64.42  
    65.1 --- a/src/FOLP/ex/quant.ML	Mon Jan 29 13:56:41 1996 +0100
    65.2 +++ b/src/FOLP/ex/quant.ML	Mon Jan 29 13:58:15 1996 +0100
    65.3 @@ -1,6 +1,6 @@
    65.4 -(*  Title: 	FOL/ex/quant
    65.5 +(*  Title:      FOL/ex/quant
    65.6      ID:         $Id$
    65.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    65.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    65.9      Copyright   1991  University of Cambridge
   65.10  
   65.11  First-Order Logic: quantifier examples (intuitionistic and classical)
    66.1 --- a/src/FOLP/hypsubst.ML	Mon Jan 29 13:56:41 1996 +0100
    66.2 +++ b/src/FOLP/hypsubst.ML	Mon Jan 29 13:58:15 1996 +0100
    66.3 @@ -1,6 +1,6 @@
    66.4 -(*  Title: 	FOLP/hypsubst
    66.5 +(*  Title:      FOLP/hypsubst
    66.6      ID:         $Id$
    66.7 -    Author: 	Martin D Coen, Cambridge University Computer Laboratory
    66.8 +    Author:     Martin D Coen, Cambridge University Computer Laboratory
    66.9      Copyright   1995  University of Cambridge
   66.10  
   66.11  Original version of Provers/hypsubst.  Cannot use new version because it
   66.12 @@ -11,11 +11,11 @@
   66.13  
   66.14  signature HYPSUBST_DATA =
   66.15    sig
   66.16 -  val dest_eq	: term -> term*term
   66.17 -  val imp_intr	: thm		(* (P ==> Q) ==> P-->Q *)
   66.18 -  val rev_mp	: thm		(* [| P;  P-->Q |] ==> Q *)
   66.19 -  val subst	: thm		(* [| a=b;  P(a) |] ==> P(b) *)
   66.20 -  val sym	: thm		(* a=b ==> b=a *)
   66.21 +  val dest_eq   : term -> term*term
   66.22 +  val imp_intr  : thm           (* (P ==> Q) ==> P-->Q *)
   66.23 +  val rev_mp    : thm           (* [| P;  P-->Q |] ==> Q *)
   66.24 +  val subst     : thm           (* [| a=b;  P(a) |] ==> P(b) *)
   66.25 +  val sym       : thm           (* a=b ==> b=a *)
   66.26    end;
   66.27  
   66.28  signature HYPSUBST =
   66.29 @@ -44,13 +44,13 @@
   66.30  fun inspect_pair bnd (t,u) =
   66.31    case (Pattern.eta_contract t, Pattern.eta_contract u) of
   66.32         (Bound i, _) => if loose(i,u) then raise Match 
   66.33 -		       else sym		(*eliminates t*)
   66.34 +                       else sym         (*eliminates t*)
   66.35       | (_, Bound i) => if loose(i,t) then raise Match 
   66.36 -		       else asm_rl	(*eliminates u*)
   66.37 +                       else asm_rl      (*eliminates u*)
   66.38       | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
   66.39 -		      else sym		(*eliminates t*)
   66.40 +                      else sym          (*eliminates t*)
   66.41       | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
   66.42 -		      else asm_rl	(*eliminates u*)
   66.43 +                      else asm_rl       (*eliminates u*)
   66.44       | _ => raise Match;
   66.45  
   66.46  (*Locates a substitutable variable on the left (resp. right) of an equality
   66.47 @@ -58,25 +58,25 @@
   66.48     the rule asm_rl (resp. sym). *)
   66.49  fun eq_var bnd =
   66.50    let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
   66.51 -	| eq_var_aux k (Const("==>",_) $ A $ B) = 
   66.52 -	      ((k, inspect_pair bnd (dest_eq A))
   66.53 -		      (*Exception Match comes from inspect_pair or dest_eq*)
   66.54 -	       handle Match => eq_var_aux (k+1) B)
   66.55 -	| eq_var_aux k _ = raise EQ_VAR
   66.56 +        | eq_var_aux k (Const("==>",_) $ A $ B) = 
   66.57 +              ((k, inspect_pair bnd (dest_eq A))
   66.58 +                      (*Exception Match comes from inspect_pair or dest_eq*)
   66.59 +               handle Match => eq_var_aux (k+1) B)
   66.60 +        | eq_var_aux k _ = raise EQ_VAR
   66.61    in  eq_var_aux 0  end;
   66.62  
   66.63  (*Select a suitable equality assumption and substitute throughout the subgoal
   66.64    Replaces only Bound variables if bnd is true*)
   66.65  fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
   66.66        let val (_,_,Bi,_) = dest_state(state,i)
   66.67 -	  val n = length(Logic.strip_assums_hyp Bi) - 1
   66.68 -	  val (k,symopt) = eq_var bnd Bi
   66.69 +          val n = length(Logic.strip_assums_hyp Bi) - 1
   66.70 +          val (k,symopt) = eq_var bnd Bi
   66.71        in 
   66.72 -	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
   66.73 -		etac revcut_rl i,
   66.74 -		REPEAT_DETERM_N (n-k) (etac rev_mp i),
   66.75 -		etac (symopt RS subst) i,
   66.76 -		REPEAT_DETERM_N n (rtac imp_intr i)]
   66.77 +         EVERY [REPEAT_DETERM_N k (etac rev_mp i),
   66.78 +                etac revcut_rl i,
   66.79 +                REPEAT_DETERM_N (n-k) (etac rev_mp i),
   66.80 +                etac (symopt RS subst) i,
   66.81 +                REPEAT_DETERM_N n (rtac imp_intr i)]
   66.82        end
   66.83        handle THM _ => no_tac | EQ_VAR => no_tac));
   66.84  
    67.1 --- a/src/FOLP/intprover.ML	Mon Jan 29 13:56:41 1996 +0100
    67.2 +++ b/src/FOLP/intprover.ML	Mon Jan 29 13:58:15 1996 +0100
    67.3 @@ -1,6 +1,6 @@
    67.4 -(*  Title: 	FOL/int-prover
    67.5 +(*  Title:      FOL/int-prover
    67.6      ID:         $Id$
    67.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    67.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    67.9      Copyright   1992  University of Cambridge
   67.10  
   67.11  A naive prover for intuitionistic logic
   67.12 @@ -54,10 +54,10 @@
   67.13  
   67.14  (*Attack subgoals using safe inferences*)
   67.15  val safe_step_tac = FIRST' [uniq_assume_tac,
   67.16 -			    IFOLP_Lemmas.uniq_mp_tac,
   67.17 -			    biresolve_tac safe0_brls,
   67.18 -			    hyp_subst_tac,
   67.19 -			    biresolve_tac safep_brls] ;
   67.20 +                            IFOLP_Lemmas.uniq_mp_tac,
   67.21 +                            biresolve_tac safe0_brls,
   67.22 +                            hyp_subst_tac,
   67.23 +                            biresolve_tac safep_brls] ;
   67.24  
   67.25  (*Repeatedly attack subgoals using safe inferences*)
   67.26  val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
    68.1 --- a/src/FOLP/simp.ML	Mon Jan 29 13:56:41 1996 +0100
    68.2 +++ b/src/FOLP/simp.ML	Mon Jan 29 13:58:15 1996 +0100
    68.3 @@ -76,13 +76,13 @@
    68.4    rewrite rules are not ordered.*)
    68.5  fun net_tac net =
    68.6    SUBGOAL(fn (prem,i) => 
    68.7 -	  resolve_tac (Net.unify_term net (strip_assums_concl prem)) i);
    68.8 +          resolve_tac (Net.unify_term net (strip_assums_concl prem)) i);
    68.9  
   68.10  (*match subgoal i against possible theorems indexed by lhs in the net*)
   68.11  fun lhs_net_tac net =
   68.12    SUBGOAL(fn (prem,i) => 
   68.13 -	  biresolve_tac (Net.unify_term net
   68.14 -		       (lhs_of (strip_assums_concl prem))) i);
   68.15 +          biresolve_tac (Net.unify_term net
   68.16 +                       (lhs_of (strip_assums_concl prem))) i);
   68.17  
   68.18  fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
   68.19  
   68.20 @@ -113,12 +113,12 @@
   68.21  val norms =
   68.22    let fun norm thm = 
   68.23        case lhs_of(concl_of thm) of
   68.24 -	  Const(n,_)$_ => n
   68.25 -	| _ => (prths normE_thms; error"No constant in lhs of a norm_thm")
   68.26 +          Const(n,_)$_ => n
   68.27 +        | _ => (prths normE_thms; error"No constant in lhs of a norm_thm")
   68.28    in map norm normE_thms end;
   68.29  
   68.30  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
   68.31 -	Const(s,_)$_ => s mem norms | _ => false;
   68.32 +        Const(s,_)$_ => s mem norms | _ => false;
   68.33  
   68.34  val refl_tac = resolve_tac refl_thms;
   68.35  
   68.36 @@ -136,7 +136,7 @@
   68.37  
   68.38  (*Applies tactic and returns the first resulting state, FAILS if none!*)
   68.39  fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
   68.40 -	Some(thm',_) => thm'
   68.41 +        Some(thm',_) => thm'
   68.42        | None => raise THM("Simplifier: could not continue", 0, [thm]);
   68.43  
   68.44  fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm);
   68.45 @@ -147,8 +147,8 @@
   68.46  (*get name of the constant from conclusion of a congruence rule*)
   68.47  fun cong_const cong = 
   68.48      case head_of (lhs_of (concl_of cong)) of
   68.49 -	Const(c,_) => c
   68.50 -      | _ => ""			(*a placeholder distinct from const names*);
   68.51 +        Const(c,_) => c
   68.52 +      | _ => ""                 (*a placeholder distinct from const names*);
   68.53  
   68.54  (*true if the term is an atomic proposition (no ==> signs) *)
   68.55  val atomic = null o strip_assums_hyp;
   68.56 @@ -156,34 +156,34 @@
   68.57  (*ccs contains the names of the constants possessing congruence rules*)
   68.58  fun add_hidden_vars ccs =
   68.59    let fun add_hvars(tm,hvars) = case tm of
   68.60 -	      Abs(_,_,body) => add_term_vars(body,hvars)
   68.61 -	    | _$_ => let val (f,args) = strip_comb tm 
   68.62 -		     in case f of
   68.63 -			    Const(c,T) => 
   68.64 -				if c mem ccs
   68.65 -				then foldr add_hvars (args,hvars)
   68.66 -				else add_term_vars(tm,hvars)
   68.67 -			  | _ => add_term_vars(tm,hvars)
   68.68 -		     end
   68.69 -	    | _ => hvars;
   68.70 +              Abs(_,_,body) => add_term_vars(body,hvars)
   68.71 +            | _$_ => let val (f,args) = strip_comb tm 
   68.72 +                     in case f of
   68.73 +                            Const(c,T) => 
   68.74 +                                if c mem ccs
   68.75 +                                then foldr add_hvars (args,hvars)
   68.76 +                                else add_term_vars(tm,hvars)
   68.77 +                          | _ => add_term_vars(tm,hvars)
   68.78 +                     end
   68.79 +            | _ => hvars;
   68.80    in add_hvars end;
   68.81  
   68.82  fun add_new_asm_vars new_asms =
   68.83      let fun itf((tm,at),vars) =
   68.84 -		if at then vars else add_term_vars(tm,vars)
   68.85 -	fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
   68.86 -		in if length(tml)=length(al)
   68.87 -		   then foldr itf (tml~~al,vars)
   68.88 -		   else vars
   68.89 -		end
   68.90 -	fun add_vars (tm,vars) = case tm of
   68.91 -		  Abs (_,_,body) => add_vars(body,vars)
   68.92 -		| r$s => (case head_of tm of
   68.93 -			  Const(c,T) => (case assoc(new_asms,c) of
   68.94 -				  None => add_vars(r,add_vars(s,vars))
   68.95 -				| Some(al) => add_list(tm,al,vars))
   68.96 -			| _ => add_vars(r,add_vars(s,vars)))
   68.97 -		| _ => vars
   68.98 +                if at then vars else add_term_vars(tm,vars)
   68.99 +        fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
  68.100 +                in if length(tml)=length(al)
  68.101 +                   then foldr itf (tml~~al,vars)
  68.102 +                   else vars
  68.103 +                end
  68.104 +        fun add_vars (tm,vars) = case tm of
  68.105 +                  Abs (_,_,body) => add_vars(body,vars)
  68.106 +                | r$s => (case head_of tm of
  68.107 +                          Const(c,T) => (case assoc(new_asms,c) of
  68.108 +                                  None => add_vars(r,add_vars(s,vars))
  68.109 +                                | Some(al) => add_list(tm,al,vars))
  68.110 +                        | _ => add_vars(r,add_vars(s,vars)))
  68.111 +                | _ => vars
  68.112      in add_vars end;
  68.113  
  68.114  
  68.115 @@ -197,27 +197,27 @@
  68.116      val hvars = foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
  68.117      val hvars = add_new_asm_vars new_asms (rhs,hvars)
  68.118      fun it_asms (asm,hvars) =
  68.119 -	if atomic asm then add_new_asm_vars new_asms (asm,hvars)
  68.120 -	else add_term_frees(asm,hvars)
  68.121 +        if atomic asm then add_new_asm_vars new_asms (asm,hvars)
  68.122 +        else add_term_frees(asm,hvars)
  68.123      val hvars = foldr it_asms (asms,hvars)
  68.124      val hvs = map (#1 o dest_Var) hvars
  68.125      val refl1_tac = refl_tac 1
  68.126      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)
  68.127 -	      (STATE(fn thm =>
  68.128 -		case head_of(rhs_of_eq 1 thm) of
  68.129 -		  Var(ixn,_) => if ixn mem hvs then refl1_tac
  68.130 -				else resolve_tac normI_thms 1 ORELSE refl1_tac
  68.131 -		| Const _ => resolve_tac normI_thms 1 ORELSE
  68.132 -			     resolve_tac congs 1 ORELSE refl1_tac
  68.133 -		| Free _ => resolve_tac congs 1 ORELSE refl1_tac
  68.134 -		| _ => refl1_tac))
  68.135 +              (STATE(fn thm =>
  68.136 +                case head_of(rhs_of_eq 1 thm) of
  68.137 +                  Var(ixn,_) => if ixn mem hvs then refl1_tac
  68.138 +                                else resolve_tac normI_thms 1 ORELSE refl1_tac
  68.139 +                | Const _ => resolve_tac normI_thms 1 ORELSE
  68.140 +                             resolve_tac congs 1 ORELSE refl1_tac
  68.141 +                | Free _ => resolve_tac congs 1 ORELSE refl1_tac
  68.142 +                | _ => refl1_tac))
  68.143      val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
  68.144  in thm'' end;
  68.145  
  68.146  fun add_norm_tags congs =
  68.147      let val ccs = map cong_const congs
  68.148 -	val new_asms = filter (exists not o #2)
  68.149 -		(ccs ~~ (map (map atomic o prems_of) congs));
  68.150 +        val new_asms = filter (exists not o #2)
  68.151 +                (ccs ~~ (map (map atomic o prems_of) congs));
  68.152      in add_norms(congs,ccs,new_asms) end;
  68.153  
  68.154  fun normed_rews congs =
  68.155 @@ -225,7 +225,7 @@
  68.156    in fn thm => map (varifyT o add_norms o mk_trans) (mk_rew_rules(freezeT thm))
  68.157    end;
  68.158  
  68.159 -fun NORM norm_lhs_tac = EVERY'[resolve_tac [red2], norm_lhs_tac, refl_tac];
  68.160 +fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac];
  68.161  
  68.162  val trans_norms = map mk_trans normE_thms;
  68.163  
  68.164 @@ -233,15 +233,15 @@
  68.165  (* SIMPSET *)
  68.166  
  68.167  datatype simpset =
  68.168 -	SS of {auto_tac: int -> tactic,
  68.169 -	       congs: thm list,
  68.170 -	       cong_net: thm Net.net,
  68.171 -	       mk_simps: thm -> thm list,
  68.172 -	       simps: (thm * thm list) list,
  68.173 -	       simp_net: thm Net.net}
  68.174 +        SS of {auto_tac: int -> tactic,
  68.175 +               congs: thm list,
  68.176 +               cong_net: thm Net.net,
  68.177 +               mk_simps: thm -> thm list,
  68.178 +               simps: (thm * thm list) list,
  68.179 +               simp_net: thm Net.net}
  68.180  
  68.181  val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty,
  68.182 -		  mk_simps=normed_rews[], simps=[], simp_net=Net.empty};
  68.183 +                  mk_simps=normed_rews[], simps=[], simp_net=Net.empty};
  68.184  
  68.185  (** Insertion of congruences and rewrites **)
  68.186  
  68.187 @@ -289,10 +289,10 @@
  68.188  
  68.189  fun delrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
  68.190  let fun find((p as (th,ths))::ps',ps) =
  68.191 -	  if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
  68.192 +          if eq_thm(thm,th) then (ths,ps@ps') else find(ps',p::ps)
  68.193        | find([],simps') = (writeln"\nNo such rewrite or congruence rule:";
  68.194 -			   print_thm thm;
  68.195 -			   ([],simps'))
  68.196 +                           print_thm thm;
  68.197 +                           ([],simps'))
  68.198      val (thms,simps') = find(simps,[])
  68.199  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
  68.200        simps = simps', simp_net = delete_thms(thms,simp_net)}
  68.201 @@ -311,8 +311,8 @@
  68.202  fun dest_ss(SS{congs,simps,...}) = (congs, map #1 simps);
  68.203  
  68.204  fun print_ss(SS{congs,simps,...}) =
  68.205 -	(writeln"Congruences:"; prths congs;
  68.206 -	 writeln"Rewrite Rules:"; prths (map #1 simps); ());
  68.207 +        (writeln"Congruences:"; prths congs;
  68.208 +         writeln"Rewrite Rules:"; prths (map #1 simps); ());
  68.209  
  68.210  
  68.211  (* Rewriting with conditionals *)
  68.212 @@ -322,32 +322,32 @@
  68.213  
  68.214  fun if_rewritable ifc i thm =
  68.215      let val tm = goal_concl i thm
  68.216 -	fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1)
  68.217 -	  | nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k)
  68.218 -	  | nobound(Bound n,j,k) = n < k orelse k+j <= n
  68.219 -	  | nobound(_) = true;
  68.220 -	fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al
  68.221 -	fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1)
  68.222 -	  | find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in
  68.223 -		case f of Const(c,_) =>	if c=ifc then check_args(al,j)
  68.224 -			else find_if(s,j) orelse find_if(t,j)
  68.225 -		| _ => find_if(s,j) orelse find_if(t,j) end
  68.226 -	  | find_if(_) = false;
  68.227 +        fun nobound(Abs(_,_,tm),j,k) = nobound(tm,j,k+1)
  68.228 +          | nobound(s$t,j,k) = nobound(s,j,k) andalso nobound(t,j,k)
  68.229 +          | nobound(Bound n,j,k) = n < k orelse k+j <= n
  68.230 +          | nobound(_) = true;
  68.231 +        fun check_args(al,j) = forall (fn t => nobound(t,j,0)) al
  68.232 +        fun find_if(Abs(_,_,tm),j) = find_if(tm,j+1)
  68.233 +          | find_if(tm as s$t,j) = let val (f,al) = strip_comb tm in
  68.234 +                case f of Const(c,_) => if c=ifc then check_args(al,j)
  68.235 +                        else find_if(s,j) orelse find_if(t,j)
  68.236 +                | _ => find_if(s,j) orelse find_if(t,j) end
  68.237 +          | find_if(_) = false;
  68.238      in find_if(tm,0) end;
  68.239  
  68.240  fun IF1_TAC cong_tac i =
  68.241      let fun seq_try (ifth::ifths,ifc::ifcs) thm = tapply(
  68.242 -		COND (if_rewritable ifc i) (DETERM(resolve_tac[ifth]i))
  68.243 -			(Tactic(seq_try(ifths,ifcs))), thm)
  68.244 -	      | seq_try([],_) thm = tapply(no_tac,thm)
  68.245 -	and try_rew thm = tapply(Tactic(seq_try(case_rews,case_consts))
  68.246 -				 ORELSE Tactic one_subt, thm)
  68.247 -	and one_subt thm =
  68.248 -		let val test = has_fewer_prems (nprems_of thm + 1)
  68.249 -		    fun loop thm = tapply(COND test no_tac
  68.250 -			((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
  68.251 -			 ORELSE (refl_tac i THEN Tactic loop)), thm)
  68.252 -		in tapply(cong_tac THEN Tactic loop, thm) end
  68.253 +                COND (if_rewritable ifc i) (DETERM(rtac ifth i))
  68.254 +                        (Tactic(seq_try(ifths,ifcs))), thm)
  68.255 +              | seq_try([],_) thm = tapply(no_tac,thm)
  68.256 +        and try_rew thm = tapply(Tactic(seq_try(case_rews,case_consts))
  68.257 +                                 ORELSE Tactic one_subt, thm)
  68.258 +        and one_subt thm =
  68.259 +                let val test = has_fewer_prems (nprems_of thm + 1)
  68.260 +                    fun loop thm = tapply(COND test no_tac
  68.261 +                        ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
  68.262 +                         ORELSE (refl_tac i THEN Tactic loop)), thm)
  68.263 +                in tapply(cong_tac THEN Tactic loop, thm) end
  68.264      in COND (may_match(case_consts,i)) (Tactic try_rew) no_tac end;
  68.265  
  68.266  fun CASE_TAC (SS{cong_net,...}) i =
  68.267 @@ -357,7 +357,7 @@
  68.268  (* Rewriting Automaton *)
  68.269  
  68.270  datatype cntrl = STOP | MK_EQ | ASMS of int | SIMP_LHS | REW | REFL | TRUE
  68.271 -	       | PROVE | POP_CS | POP_ARTR | IF;
  68.272 +               | PROVE | POP_CS | POP_ARTR | IF;
  68.273  (*
  68.274  fun pr_cntrl c = case c of STOP => prs("STOP") | MK_EQ => prs("MK_EQ") |
  68.275  ASMS i => print_int i | POP_ARTR => prs("POP_ARTR") |
  68.276 @@ -367,7 +367,7 @@
  68.277  *)
  68.278  fun simp_refl([],_,ss) = ss
  68.279    | simp_refl(a'::ns,a,ss) = if a'=a then simp_refl(ns,a,SIMP_LHS::REFL::ss)
  68.280 -	else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss);
  68.281 +        else simp_refl(ns,a,ASMS(a)::SIMP_LHS::REFL::POP_ARTR::ss);
  68.282  
  68.283  (** Tracing **)
  68.284  
  68.285 @@ -381,13 +381,13 @@
  68.286  (*Select subgoal i from proof state; substitute parameters, for printing*)
  68.287  fun prepare_goal i st =
  68.288      let val subgi = nth_subgoal i st
  68.289 -	val params = rev(strip_params subgi)
  68.290 +        val params = rev(strip_params subgi)
  68.291      in variants_abs (params, strip_assums_concl subgi) end;
  68.292  
  68.293  (*print lhs of conclusion of subgoal i*)
  68.294  fun pr_goal_lhs i st =
  68.295      writeln (Sign.string_of_term (#sign(rep_thm st)) 
  68.296 -	     (lhs_of (prepare_goal i st)));
  68.297 +             (lhs_of (prepare_goal i st)));
  68.298  
  68.299  (*print conclusion of subgoal i*)
  68.300  fun pr_goal_concl i st =
  68.301 @@ -404,17 +404,17 @@
  68.302      if !tracing
  68.303      then (if not_asms then () else writeln"Assumption used in";
  68.304            pr_goal_lhs i thm; writeln"->"; pr_goal_lhs (i+n) thm';
  68.305 -	  if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm')
  68.306 +          if n>0 then (writeln"Conditions:"; pr_goals (i, i+n-1) thm')
  68.307            else ();
  68.308            writeln"" )
  68.309      else ();
  68.310  
  68.311  (* Skip the first n hyps of a goal, and return the rest in generalized form *)
  68.312  fun strip_varify(Const("==>", _) $ H $ B, n, vs) =
  68.313 -	if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
  68.314 -	else strip_varify(B,n-1,vs)
  68.315 +        if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
  68.316 +        else strip_varify(B,n-1,vs)
  68.317    | strip_varify(Const("all",_)$Abs(_,T,t), n, vs) =
  68.318 -	strip_varify(t,n,Var(("?",length vs),T)::vs)
  68.319 +        strip_varify(t,n,Var(("?",length vs),T)::vs)
  68.320    | strip_varify  _  = [];
  68.321  
  68.322  fun execute(ss,if_fl,auto_tac,cong_tac,net,i,thm) = let
  68.323 @@ -423,73 +423,73 @@
  68.324      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
  68.325      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
  68.326      else case Sequence.pull(tapply(cong_tac i,thm)) of
  68.327 -	    Some(thm',_) =>
  68.328 -		    let val ps = prems_of thm and ps' = prems_of thm';
  68.329 -			val n = length(ps')-length(ps);
  68.330 -			val a = length(strip_assums_hyp(nth_elem(i-1,ps)))
  68.331 -			val l = map (fn p => length(strip_assums_hyp(p)))
  68.332 -				    (take(n,drop(i-1,ps')));
  68.333 -		    in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
  68.334 -	  | None => (REW::ss,thm,anet,ats,cs);
  68.335 +            Some(thm',_) =>
  68.336 +                    let val ps = prems_of thm and ps' = prems_of thm';
  68.337 +                        val n = length(ps')-length(ps);
  68.338 +                        val a = length(strip_assums_hyp(nth_elem(i-1,ps)))
  68.339 +                        val l = map (fn p => length(strip_assums_hyp(p)))
  68.340 +                                    (take(n,drop(i-1,ps')));
  68.341 +                    in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
  68.342 +          | None => (REW::ss,thm,anet,ats,cs);
  68.343  
  68.344  (*NB: the "Adding rewrites:" trace will look strange because assumptions
  68.345        are represented by rules, generalized over their parameters*)
  68.346  fun add_asms(ss,thm,a,anet,ats,cs) =
  68.347      let val As = strip_varify(nth_subgoal i thm, a, []);
  68.348 -	val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
  68.349 -	val new_rws = flat(map mk_rew_rules thms);
  68.350 -	val rwrls = map mk_trans (flat(map mk_rew_rules thms));
  68.351 -	val anet' = foldr lhs_insert_thm (rwrls,anet)
  68.352 +        val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
  68.353 +        val new_rws = flat(map mk_rew_rules thms);
  68.354 +        val rwrls = map mk_trans (flat(map mk_rew_rules thms));
  68.355 +        val anet' = foldr lhs_insert_thm (rwrls,anet)
  68.356      in  if !tracing andalso not(null new_rws)
  68.357 -	then (writeln"Adding rewrites:";  prths new_rws;  ())
  68.358 -	else ();
  68.359 -	(ss,thm,anet',anet::ats,cs) 
  68.360 +        then (writeln"Adding rewrites:";  prths new_rws;  ())
  68.361 +        else ();
  68.362 +        (ss,thm,anet',anet::ats,cs) 
  68.363      end;
  68.364  
  68.365  fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of
  68.366        Some(thm',seq') =>
  68.367 -	    let val n = (nprems_of thm') - (nprems_of thm)
  68.368 -	    in pr_rew(i,n,thm,thm',more);
  68.369 -	       if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
  68.370 -	       else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
  68.371 -		     thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
  68.372 -	    end
  68.373 +            let val n = (nprems_of thm') - (nprems_of thm)
  68.374 +            in pr_rew(i,n,thm,thm',more);
  68.375 +               if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
  68.376 +               else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
  68.377 +                     thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
  68.378 +            end
  68.379      | None => if more
  68.380 -	    then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),
  68.381 -		     thm,ss,anet,ats,cs,false)
  68.382 -	    else (ss,thm,anet,ats,cs);
  68.383 +            then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),
  68.384 +                     thm,ss,anet,ats,cs,false)
  68.385 +            else (ss,thm,anet,ats,cs);
  68.386  
  68.387  fun try_true(thm,ss,anet,ats,cs) =
  68.388      case Sequence.pull(tapply(auto_tac i,thm)) of
  68.389        Some(thm',_) => (ss,thm',anet,ats,cs)
  68.390      | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
  68.391 -	      in if !tracing
  68.392 -		 then (writeln"*** Failed to prove precondition. Normal form:";
  68.393 -		       pr_goal_concl i thm;  writeln"")
  68.394 -		 else ();
  68.395 -		 rew(seq,thm0,ss0,anet0,ats0,cs0,more)
  68.396 -	      end;
  68.397 +              in if !tracing
  68.398 +                 then (writeln"*** Failed to prove precondition. Normal form:";
  68.399 +                       pr_goal_concl i thm;  writeln"")
  68.400 +                 else ();
  68.401 +                 rew(seq,thm0,ss0,anet0,ats0,cs0,more)
  68.402 +              end;
  68.403  
  68.404  fun if_exp(thm,ss,anet,ats,cs) =
  68.405 -	case Sequence.pull(tapply(IF1_TAC (cong_tac i) i,thm)) of
  68.406 -		Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
  68.407 -	      | None => (ss,thm,anet,ats,cs);
  68.408 +        case Sequence.pull(tapply(IF1_TAC (cong_tac i) i,thm)) of
  68.409 +                Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
  68.410 +              | None => (ss,thm,anet,ats,cs);
  68.411  
  68.412  fun step(s::ss, thm, anet, ats, cs) = case s of
  68.413 -	  MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
  68.414 -	| ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
  68.415 -	| SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
  68.416 -	| REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
  68.417 -	| REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
  68.418 -	| TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
  68.419 -	| PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss
  68.420 -		    else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs)
  68.421 -	| POP_ARTR => (ss,thm,hd ats,tl ats,cs)
  68.422 -	| POP_CS => (ss,thm,anet,ats,tl cs)
  68.423 -	| IF => if_exp(thm,ss,anet,ats,cs);
  68.424 +          MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
  68.425 +        | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
  68.426 +        | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
  68.427 +        | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
  68.428 +        | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
  68.429 +        | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
  68.430 +        | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss
  68.431 +                    else MK_EQ::SIMP_LHS::TRUE::ss, thm, anet, ats, cs)
  68.432 +        | POP_ARTR => (ss,thm,hd ats,tl ats,cs)
  68.433 +        | POP_CS => (ss,thm,anet,ats,tl cs)
  68.434 +        | IF => if_exp(thm,ss,anet,ats,cs);
  68.435  
  68.436  fun exec(state as (s::ss, thm, _, _, _)) =
  68.437 -	if s=STOP then thm else exec(step(state));
  68.438 +        if s=STOP then thm else exec(step(state));
  68.439  
  68.440  in exec(ss, thm, Net.empty, [], []) end;
  68.441  
  68.442 @@ -497,9 +497,9 @@
  68.443  fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
  68.444  let val cong_tac = net_tac cong_net
  68.445  in fn i => Tactic(fn thm =>
  68.446 -	if i <= 0 orelse nprems_of thm < i then Sequence.null
  68.447 -	else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
  68.448 -	   THEN TRY(auto_tac i)
  68.449 +        if i <= 0 orelse nprems_of thm < i then Sequence.null
  68.450 +        else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
  68.451 +           THEN TRY(auto_tac i)
  68.452  end;
  68.453  
  68.454  val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false);
  68.455 @@ -513,7 +513,7 @@
  68.456  fun REWRITE (ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
  68.457  let val cong_tac = net_tac cong_net
  68.458  in fn thm => let val state = thm RSN (2,red1)
  68.459 -	     in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end
  68.460 +             in execute(ss,fl,auto_tac,cong_tac,simp_net,1,state) end
  68.461  end;
  68.462  
  68.463  val SIMP_THM = REWRITE ([ASMS(0),SIMP_LHS,IF,REFL,STOP],false);
  68.464 @@ -529,7 +529,7 @@
  68.465    | exp_app(i,t) = exp_app(i-1,t $ Bound (i-1));
  68.466  
  68.467  fun exp_abs(Type("fun",[T1,T2]),t,i) =
  68.468 -	Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1))
  68.469 +        Abs("x"^string_of_int i,T1,exp_abs(T2,t,i+1))
  68.470    | exp_abs(T,t,i) = exp_app(i,t);
  68.471  
  68.472  fun eta_Var(ixn,T) = exp_abs(T,Var(ixn,T),0);
  68.473 @@ -537,20 +537,20 @@
  68.474  
  68.475  fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
  68.476  let fun xn_list(x,n) =
  68.477 -	let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
  68.478 -	in map eta_Var (ixs ~~ (take(n+1,Ts))) end
  68.479 +        let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
  68.480 +        in map eta_Var (ixs ~~ (take(n+1,Ts))) end
  68.481      val lhs = list_comb(f,xn_list("X",k-1))
  68.482      val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
  68.483  in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
  68.484  
  68.485  fun find_subst tsig T =
  68.486  let fun find (thm::thms) =
  68.487 -	let val (Const(_,cT), va, vb) =	dest_red(hd(prems_of thm));
  68.488 -	    val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
  68.489 -	    val eqT::_ = binder_types cT
  68.490 +        let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
  68.491 +            val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
  68.492 +            val eqT::_ = binder_types cT
  68.493          in if Type.typ_instance(tsig,T,eqT) then Some(thm,va,vb,P)
  68.494 -	   else find thms
  68.495 -	end
  68.496 +           else find thms
  68.497 +        end
  68.498        | find [] = None
  68.499  in find subst_thms end;
  68.500  
  68.501 @@ -558,20 +558,20 @@
  68.502  let val tsig = #tsig(Sign.rep_sg sg);
  68.503      val k = length aTs;
  68.504      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
  68.505 -	let val ca = cterm_of sg va
  68.506 -	    and cx = cterm_of sg (eta_Var(("X"^si,0),T))
  68.507 -	    val cb = cterm_of sg vb
  68.508 -	    and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
  68.509 -	    val cP = cterm_of sg P
  68.510 -	    and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
  68.511 -	in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
  68.512 +        let val ca = cterm_of sg va
  68.513 +            and cx = cterm_of sg (eta_Var(("X"^si,0),T))
  68.514 +            val cb = cterm_of sg vb
  68.515 +            and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
  68.516 +            val cP = cterm_of sg P
  68.517 +            and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
  68.518 +        in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
  68.519      fun mk(c,T::Ts,i,yik) =
  68.520 -	let val si = radixstring(26,"a",i)
  68.521 -	in case find_subst tsig T of
  68.522 -	     None => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik)
  68.523 -	   | Some s => let val c' = c RSN (2,ri(s,i,si,T,yik))
  68.524 -		       in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end
  68.525 -	end
  68.526 +        let val si = radixstring(26,"a",i)
  68.527 +        in case find_subst tsig T of
  68.528 +             None => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik)
  68.529 +           | Some s => let val c' = c RSN (2,ri(s,i,si,T,yik))
  68.530 +                       in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end
  68.531 +        end
  68.532        | mk(c,[],_,_) = c;
  68.533  in mk(refl,rev aTs,k-1,[]) end;
  68.534  
  68.535 @@ -579,10 +579,10 @@
  68.536  let val (aTs,rT) = strip_type T;
  68.537      val tsig = #tsig(Sign.rep_sg sg);
  68.538      fun find_refl(r::rs) =
  68.539 -	let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
  68.540 -	in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
  68.541 -	   then Some(r,(eq,body_type eqT)) else find_refl rs
  68.542 -	end
  68.543 +        let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
  68.544 +        in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
  68.545 +           then Some(r,(eq,body_type eqT)) else find_refl rs
  68.546 +        end
  68.547        | find_refl([]) = None;
  68.548  in case find_refl refl_thms of
  68.549       None => []  |  Some(refl) => [mk_cong sg (f,aTs,rT) refl]
  68.550 @@ -591,7 +591,7 @@
  68.551  fun mk_cong_thy thy f =
  68.552  let val sg = sign_of thy;
  68.553      val T = case Sign.const_type sg f of
  68.554 -		None => error(f^" not declared") | Some(T) => T;
  68.555 +                None => error(f^" not declared") | Some(T) => T;
  68.556      val T' = incr_tvar 9 T;
  68.557  in mk_cong_type sg (Const(f,T'),T') end;
  68.558  
  68.559 @@ -601,10 +601,10 @@
  68.560  let val sg = sign_of thy;
  68.561      val S0 = Type.defaultS(#tsig(Sign.rep_sg sg))
  68.562      fun readfT(f,s) =
  68.563 -	let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
  68.564 -	    val t = case Sign.const_type sg f of
  68.565 -		      Some(_) => Const(f,T) | None => Free(f,T)
  68.566 -	in (t,T) end
  68.567 +        let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
  68.568 +            val t = case Sign.const_type sg f of
  68.569 +                      Some(_) => Const(f,T) | None => Free(f,T)
  68.570 +        in (t,T) end
  68.571  in flat o map (mk_cong_type sg o readfT) end;
  68.572  
  68.573  end (* local *)
    69.1 --- a/src/FOLP/simpdata.ML	Mon Jan 29 13:56:41 1996 +0100
    69.2 +++ b/src/FOLP/simpdata.ML	Mon Jan 29 13:58:15 1996 +0100
    69.3 @@ -1,6 +1,6 @@
    69.4 -(*  Title: 	FOL/simpdata
    69.5 +(*  Title:      FOL/simpdata
    69.6      ID:         $Id$
    69.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    69.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    69.9      Copyright   1991  University of Cambridge
   69.10  
   69.11  Simplification data for FOL
   69.12 @@ -15,33 +15,33 @@
   69.13  fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
   69.14  
   69.15  val conj_rews = map int_prove_fun
   69.16 - ["P & True <-> P", 	"True & P <-> P",
   69.17 + ["P & True <-> P",     "True & P <-> P",
   69.18    "P & False <-> False", "False & P <-> False",
   69.19    "P & P <-> P",
   69.20 -  "P & ~P <-> False", 	"~P & P <-> False",
   69.21 +  "P & ~P <-> False",   "~P & P <-> False",
   69.22    "(P & Q) & R <-> P & (Q & R)"];
   69.23  
   69.24  val disj_rews = map int_prove_fun
   69.25 - ["P | True <-> True", 	"True | P <-> True",
   69.26 -  "P | False <-> P", 	"False | P <-> P",
   69.27 + ["P | True <-> True",  "True | P <-> True",
   69.28 +  "P | False <-> P",    "False | P <-> P",
   69.29    "P | P <-> P",
   69.30    "(P | Q) | R <-> P | (Q | R)"];
   69.31  
   69.32  val not_rews = map int_prove_fun
   69.33 - ["~ False <-> True",	"~ True <-> False"];
   69.34 + ["~ False <-> True",   "~ True <-> False"];
   69.35  
   69.36  val imp_rews = map int_prove_fun
   69.37 - ["(P --> False) <-> ~P",	"(P --> True) <-> True",
   69.38 -  "(False --> P) <-> True",	"(True --> P) <-> P", 
   69.39 -  "(P --> P) <-> True",		"(P --> ~P) <-> ~P"];
   69.40 + ["(P --> False) <-> ~P",       "(P --> True) <-> True",
   69.41 +  "(False --> P) <-> True",     "(True --> P) <-> P", 
   69.42 +  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
   69.43  
   69.44  val iff_rews = map int_prove_fun
   69.45 - ["(True <-> P) <-> P", 	"(P <-> True) <-> P",
   69.46 + ["(True <-> P) <-> P",         "(P <-> True) <-> P",
   69.47    "(P <-> P) <-> True",
   69.48 -  "(False <-> P) <-> ~P", 	"(P <-> False) <-> ~P"];
   69.49 +  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
   69.50  
   69.51  val quant_rews = map int_prove_fun
   69.52 - ["(ALL x.P) <-> P",	"(EX x.P) <-> P"];
   69.53 + ["(ALL x.P) <-> P",    "(EX x.P) <-> P"];
   69.54  
   69.55  (*These are NOT supplied by default!*)
   69.56  val distrib_rews  = map int_prove_fun
   69.57 @@ -60,7 +60,7 @@
   69.58  val refl_iff_T = make_iff_T refl;
   69.59  
   69.60  val norm_thms = [(norm_eq RS sym, norm_eq),
   69.61 -		 (NORM_iff RS iff_sym, NORM_iff)];
   69.62 +                 (NORM_iff RS iff_sym, NORM_iff)];
   69.63  
   69.64  
   69.65  (* Conversion into rewrite rules *)
   69.66 @@ -76,7 +76,7 @@
   69.67  fun atomize th = case concl_of th of (*The operator below is "Proof $ P $ p"*)
   69.68        _ $ (Const("op -->",_) $ _ $ _) $ _ => atomize(th RS mp)
   69.69      | _ $ (Const("op &",_) $ _ $ _) $ _ => atomize(th RS conjunct1) @
   69.70 -				       atomize(th RS conjunct2)
   69.71 +                                       atomize(th RS conjunct2)
   69.72      | _ $ (Const("All",_) $ _) $ _ => atomize(th RS spec)
   69.73      | _ $ (Const("True",_)) $ _ => []
   69.74      | _ $ (Const("False",_)) $ _ => []
   69.75 @@ -90,15 +90,15 @@
   69.76  
   69.77  structure FOLP_SimpData : SIMP_DATA =
   69.78    struct
   69.79 -  val refl_thms		= [refl, iff_refl]
   69.80 -  val trans_thms	= [trans, iff_trans]
   69.81 -  val red1		= iffD1
   69.82 -  val red2		= iffD2
   69.83 -  val mk_rew_rules	= mk_rew_rules
   69.84 -  val case_splits	= []         (*NO IF'S!*)
   69.85 -  val norm_thms		= norm_thms
   69.86 -  val subst_thms	= [subst];
   69.87 -  val dest_red		= dest_red
   69.88 +  val refl_thms         = [refl, iff_refl]
   69.89 +  val trans_thms        = [trans, iff_trans]
   69.90 +  val red1              = iffD1
   69.91 +  val red2              = iffD2
   69.92 +  val mk_rew_rules      = mk_rew_rules
   69.93 +  val case_splits       = []         (*NO IF'S!*)
   69.94 +  val norm_thms         = norm_thms
   69.95 +  val subst_thms        = [subst];
   69.96 +  val dest_red          = dest_red
   69.97    end;
   69.98  
   69.99  structure FOLP_Simp = SimpFun(FOLP_SimpData);
  69.100 @@ -124,8 +124,8 @@
  69.101         (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
  69.102  
  69.103  val cla_rews = map prove_fun
  69.104 - ["?p:P | ~P", 		"?p:~P | P",
  69.105 -  "?p:~ ~ P <-> P",	"?p:(~P --> P) <-> P"];
  69.106 + ["?p:P | ~P",          "?p:~P | P",
  69.107 +  "?p:~ ~ P <-> P",     "?p:(~P --> P) <-> P"];
  69.108  
  69.109  val FOLP_rews = IFOLP_rews@cla_rews;
  69.110