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