equal
deleted
inserted
replaced
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 (* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *) |
5 (* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *) |
6 signature CONTEXT_C = |
6 signature CONTEXT_C = |
7 sig |
7 sig |
8 val e_ctxt : Proof.context |
8 val empty : Proof.context |
9 val is_e_ctxt : Proof.context -> bool |
9 val is_empty : Proof.context -> bool |
10 val isac_ctxt : 'a -> Proof.context |
10 val isac_ctxt : 'a -> Proof.context |
11 val declare_constraints: term -> Proof.context -> Proof.context |
11 val declare_constraints: term -> Proof.context -> Proof.context |
12 val initialise : string -> term list -> Proof.context |
12 val initialise : string -> term list -> Proof.context |
13 val initialise' : theory -> string list -> Proof.context |
13 val initialise' : theory -> string list -> Proof.context |
14 val get_assumptions : Proof.context -> term list |
14 val get_assumptions : Proof.context -> term list |
26 end |
26 end |
27 |
27 |
28 structure ContextC(**) : CONTEXT_C(**) = |
28 structure ContextC(**) : CONTEXT_C(**) = |
29 struct |
29 struct |
30 |
30 |
31 val e_ctxt = Proof_Context.init_global @{theory "Pure"}; |
31 val empty = Proof_Context.init_global @{theory "Pure"}; |
32 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*) |
32 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*) |
33 fun is_e_ctxt ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"}); |
33 fun is_empty ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"}); |
34 fun isac_ctxt xxx = Proof_Context.init_global (Rule.Isac xxx) |
34 fun isac_ctxt xxx = Proof_Context.init_global (Rule.Isac xxx) |
35 |
35 |
36 val declare_constraints = Variable.declare_constraints |
36 val declare_constraints = Variable.declare_constraints |
37 (* in Subproblem take respective actual arguments from program *) |
37 (* in Subproblem take respective actual arguments from program *) |
38 fun initialise thy' ts = |
38 fun initialise thy' ts = |