equal
deleted
inserted
replaced
101 in |
101 in |
102 |
102 |
103 val includes = gen_includes (K I); |
103 val includes = gen_includes (K I); |
104 val includes_cmd = gen_includes check; |
104 val includes_cmd = gen_includes check; |
105 |
105 |
106 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.put_facts NONE; |
106 fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts; |
107 fun include_cmd bs = |
107 fun include_cmd bs = |
108 Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.put_facts NONE; |
108 Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts; |
109 |
109 |
110 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); |
110 fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); |
111 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs); |
111 fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs); |
112 |
112 |
113 val context_includes = gen_context (K I); |
113 val context_includes = gen_context (K I); |