equal
deleted
inserted
replaced
135 |
135 |
136 fun map_current f (State ({context, facts, mode, goal}, nodes)) = |
136 fun map_current f (State ({context, facts, mode, goal}, nodes)) = |
137 State (make_node (f (context, facts, mode, goal)), nodes); |
137 State (make_node (f (context, facts, mode, goal)), nodes); |
138 |
138 |
139 fun init_state thy = |
139 fun init_state thy = |
140 State (make_node (ProofContext.init_context thy, None, Forward, None), []); |
140 State (make_node (ProofContext.init thy, None, Forward, None), []); |
141 |
141 |
142 |
142 |
143 |
143 |
144 (** basic proof state operations **) |
144 (** basic proof state operations **) |
145 |
145 |