src/HOL/Integ/int_arith1.ML
changeset 15531 08c8dad8e399
parent 15185 8c43ffe2bb32
child 15661 9ef583b08647
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -93,10 +93,10 @@
     1.4  structure Bin_Simprocs =
     1.5    struct
     1.6    fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
     1.7 -    if t aconv u then None
     1.8 +    if t aconv u then NONE
     1.9      else
    1.10        let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    1.11 -      in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
    1.12 +      in SOME (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
    1.13  
    1.14    fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
    1.15    fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
    1.16 @@ -119,10 +119,10 @@
    1.17      0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
    1.18    fun reorient_proc sg _ (_ $ t $ u) =
    1.19      case u of
    1.20 -	Const("0", _) => None
    1.21 -      | Const("1", _) => None
    1.22 -      | Const("Numeral.number_of", _) $ _ => None
    1.23 -      | _ => Some (case t of
    1.24 +	Const("0", _) => NONE
    1.25 +      | Const("1", _) => NONE
    1.26 +      | Const("Numeral.number_of", _) $ _ => NONE
    1.27 +      | _ => SOME (case t of
    1.28  		  Const("0", _) => meta_zero_reorient
    1.29  		| Const("1", _) => meta_one_reorient
    1.30  		| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
    1.31 @@ -305,8 +305,8 @@
    1.32      [mult_assoc, minus_mult_left, minus_mult_eq_1_to_2];
    1.33  
    1.34  (*Apply the given rewrite (if present) just once*)
    1.35 -fun trans_tac None      = all_tac
    1.36 -  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
    1.37 +fun trans_tac NONE      = all_tac
    1.38 +  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
    1.39  
    1.40  fun simplify_meta_eq rules =
    1.41      simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
    1.42 @@ -538,7 +538,7 @@
    1.43  Addsimprocs [fast_int_arith_simproc]
    1.44  
    1.45  
    1.46 -(* Some test data
    1.47 +(* SOME test data
    1.48  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
    1.49  by (fast_arith_tac 1);
    1.50  Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";