equal
deleted
inserted
replaced
214 val ((goal_state, afterqed), lthy') = |
214 val ((goal_state, afterqed), lthy') = |
215 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
215 prepare_nominal_function do_print prep default_constraint fixspec eqns config lthy |
216 in |
216 in |
217 lthy' |
217 lthy' |
218 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
218 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
219 |> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd |
219 |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd |
220 end |
220 end |
221 |
221 |
222 val nominal_function = |
222 val nominal_function = |
223 gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
223 gen_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
224 fun nominal_function_cmd a b c int = |
224 fun nominal_function_cmd a b c int = |