src/Provers/typedsimp.ML
changeset 32957 675c0c7e6a37
parent 30190 479806475f3c
child 32960 69916a850301
equal deleted inserted replaced
32956:c39860141415 32957:675c0c7e6a37
    41 in
    41 in
    42 
    42 
    43 (*For simplifying both sides of an equation:
    43 (*For simplifying both sides of an equation:
    44       [| a=c; b=c |] ==> b=a
    44       [| a=c; b=c |] ==> b=a
    45   Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
    45   Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
    46 val split_eqn = standard (sym RSN (2,trans) RS sym);
    46 val split_eqn = Drule.standard (sym RSN (2,trans) RS sym);
    47 
    47 
    48 
    48 
    49 (*    [| a=b; b=c |] ==> reduce(a,c)  *)
    49 (*    [| a=b; b=c |] ==> reduce(a,c)  *)
    50 val red_trans = standard (trans RS red_if_equal);
    50 val red_trans = Drule.standard (trans RS red_if_equal);
    51 
    51 
    52 (*For REWRITE rule: Make a reduction rule for simplification, e.g.
    52 (*For REWRITE rule: Make a reduction rule for simplification, e.g.
    53   [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
    53   [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
    54 fun simp_rule rl = rl RS trans;
    54 fun simp_rule rl = rl RS trans;
    55 
    55