src/Provers/typedsimp.ML
 changeset 32957 675c0c7e6a37 parent 30190 479806475f3c child 32960 69916a850301
equal 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 `