src/HOL/simpdata.ML
 changeset 1465 5d7a7e439cec parent 1264 3eb91524b938 child 1485 240cc98b94a7
```     1.1 --- a/src/HOL/simpdata.ML	Tue Jan 30 15:19:20 1996 +0100
1.2 +++ b/src/HOL/simpdata.ML	Tue Jan 30 15:24:36 1996 +0100
1.3 @@ -1,6 +1,6 @@
1.4 -(*  Title: 	HOL/simpdata.ML
1.5 +(*  Title:      HOL/simpdata.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  Instantiation of the generic simplifier
1.12 @@ -32,9 +32,9 @@
1.13    in atoms end;
1.14
1.15  fun mk_meta_eq r = case concl_of r of
1.16 -	Const("==",_)\$_\$_ => r
1.17 -    |	_\$(Const("op =",_)\$_\$_) => r RS eq_reflection
1.18 -    |	_\$(Const("not",_)\$_) => r RS not_P_imp_P_eq_False
1.19 +        Const("==",_)\$_\$_ => r
1.20 +    |   _\$(Const("op =",_)\$_\$_) => r RS eq_reflection
1.21 +    |   _\$(Const("not",_)\$_) => r RS not_P_imp_P_eq_False
1.22      |   _ => r RS P_imp_P_eq_True;
1.23  (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
1.24
1.25 @@ -42,7 +42,7 @@
1.26
1.27  val imp_cong = impI RSN
1.28      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
1.29 -	(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
1.30 +        (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
1.31
1.32  val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
1.33   (fn _ => [rtac refl 1]);
1.34 @@ -86,9 +86,9 @@
1.35  val expand_if = prove_goal HOL.thy
1.36      "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
1.37   (fn _=> [ (res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1),
1.38 -	 rtac (if_P RS ssubst) 2,
1.39 -	 rtac (if_not_P RS ssubst) 1,
1.40 -	 REPEAT(fast_tac HOL_cs 1) ]);
1.41 +         rtac (if_P RS ssubst) 2,
1.42 +         rtac (if_not_P RS ssubst) 1,
1.43 +         REPEAT(fast_tac HOL_cs 1) ]);
1.44
1.45  val if_bool_eq = prove_goal HOL.thy
1.46                     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
1.47 @@ -141,7 +141,7 @@
1.48
1.49  val conj_cong = impI RSN
1.50      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
1.51 -	(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
1.52 +        (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
1.53
1.54  (** 'if' congruence rules: neither included by default! *)
1.55
```