equal
deleted
inserted
replaced
100 (* goals *) |
100 (* goals *) |
101 |
101 |
102 local |
102 local |
103 |
103 |
104 fun local_goal opt_chain goal stmt int = |
104 fun local_goal opt_chain goal stmt int = |
105 opt_chain #> goal (K (K Seq.single)) stmt int; |
105 opt_chain #> goal NONE (K (K Seq.single)) stmt int; |
106 |
106 |
107 fun global_goal goal kind a propp thy = |
107 fun global_goal goal kind a propp thy = |
108 goal kind (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy); |
108 goal kind NONE (K (K I)) (SOME "") a [(("", []), [propp])] (ProofContext.init thy); |
109 |
109 |
110 in |
110 in |
111 |
111 |
112 val have = local_goal I Proof.have; |
112 val have = local_goal I Proof.have; |
113 val hence = local_goal Proof.chain Proof.have; |
113 val hence = local_goal Proof.chain Proof.have; |