src/HOL/HOL.ML
changeset 1465 5d7a7e439cec
parent 1455 52a0271621f3
child 1485 240cc98b94a7
     1.1 --- a/src/HOL/HOL.ML	Tue Jan 30 15:19:20 1996 +0100
     1.2 +++ b/src/HOL/HOL.ML	Tue Jan 30 15:24:36 1996 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*  Title: 	HOL/HOL.ML
     1.5 +(*  Title:      HOL/HOL.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Tobias Nipkow
     1.8 +    Author:     Tobias Nipkow
     1.9      Copyright   1991  University of Cambridge
    1.10  
    1.11 -For hol.thy
    1.12 +For HOL.thy
    1.13  Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 
    1.14  *)
    1.15  
    1.16 @@ -20,12 +20,12 @@
    1.17  
    1.18  qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t"
    1.19   (fn prems =>
    1.20 -	[rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
    1.21 +        [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
    1.22  
    1.23  (*Useful with eresolve_tac for proving equalties from known equalities.
    1.24 -	a = b
    1.25 -	|   |
    1.26 -	c = d	*)
    1.27 +        a = b
    1.28 +        |   |
    1.29 +        c = d   *)
    1.30  qed_goal "box_equals" HOL.thy
    1.31      "[| a=b;  a=c;  b=d |] ==> c=d"  
    1.32   (fn prems=>
    1.33 @@ -57,7 +57,7 @@
    1.34  
    1.35  qed_goal "iffD2" HOL.thy "[| P=Q; Q |] ==> P"
    1.36   (fn prems =>
    1.37 -	[rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
    1.38 +        [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
    1.39  
    1.40  val iffD1 = sym RS iffD2;
    1.41  
    1.42 @@ -160,8 +160,8 @@
    1.43  
    1.44  qed_goal "conjE" HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
    1.45   (fn prems =>
    1.46 -	 [cut_facts_tac prems 1, resolve_tac prems 1,
    1.47 -	  etac conjunct1 1, etac conjunct2 1]);
    1.48 +         [cut_facts_tac prems 1, resolve_tac prems 1,
    1.49 +          etac conjunct1 1, etac conjunct2 1]);
    1.50  
    1.51  (** Disjunction *)
    1.52  
    1.53 @@ -173,8 +173,8 @@
    1.54  
    1.55  qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
    1.56   (fn [a1,a2,a3] =>
    1.57 -	[rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
    1.58 -	 rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
    1.59 +        [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
    1.60 +         rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
    1.61  
    1.62  (** CCONTR -- classical logic **)
    1.63  
    1.64 @@ -211,13 +211,13 @@
    1.65  qed_goal "selectI2" HOL.thy
    1.66      "[| P(a);  !!x. P(x) ==> Q(x) |] ==> Q(@x.P(x))"
    1.67   (fn prems => [ resolve_tac prems 1, 
    1.68 -	        rtac selectI 1, 
    1.69 -		resolve_tac prems 1 ]);
    1.70 +                rtac selectI 1, 
    1.71 +                resolve_tac prems 1 ]);
    1.72  
    1.73  qed_goal "select_equality" HOL.thy
    1.74      "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a"
    1.75   (fn prems => [ rtac selectI2 1, 
    1.76 -		REPEAT (ares_tac prems 1) ]);
    1.77 +                REPEAT (ares_tac prems 1) ]);
    1.78  
    1.79  
    1.80  (** Classical intro rules for disjunction and existential quantifiers *)
    1.81 @@ -247,7 +247,7 @@
    1.82   (fn major::prems =>
    1.83    [ (rtac (major RS iffE) 1),
    1.84      (REPEAT (DEPTH_SOLVE_1 
    1.85 -	(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
    1.86 +        (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
    1.87  
    1.88  qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x.P(x)"
    1.89   (fn prems=>
    1.90 @@ -292,10 +292,10 @@
    1.91  (*** Applying ClassicalFun to create a classical prover ***)
    1.92  structure Classical_Data = 
    1.93    struct
    1.94 -  val sizef	= size_of_thm
    1.95 -  val mp	= mp
    1.96 -  val not_elim	= notE
    1.97 -  val classical	= classical
    1.98 +  val sizef     = size_of_thm
    1.99 +  val mp        = mp
   1.100 +  val not_elim  = notE
   1.101 +  val classical = classical
   1.102    val hyp_subst_tacs=[hyp_subst_tac]
   1.103    end;
   1.104