equal
deleted
inserted
replaced
12 |
12 |
13 (*interpretation in proofs*) |
13 (*interpretation in proofs*) |
14 val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state |
14 val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state |
15 val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state |
15 val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state |
16 |
16 |
17 (*algebraic-view*) |
17 (*algebraic view*) |
18 val global_interpretation: Expression.expression_i -> |
18 val global_interpretation: Expression.expression_i -> |
19 term defines -> term rewrites -> theory -> Proof.state |
19 term defines -> term rewrites -> theory -> Proof.state |
20 val global_sublocale: string -> Expression.expression_i -> |
20 val global_sublocale: string -> Expression.expression_i -> |
21 term defines -> term rewrites -> theory -> Proof.state |
21 term defines -> term rewrites -> theory -> Proof.state |
22 val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> |
22 val global_sublocale_cmd: xstring * Position.T -> Expression.expression -> |