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
```