equal
deleted
inserted
replaced
203 lthy' |
203 lthy' |
204 |> afterqed [[pattern_thm]] |
204 |> afterqed [[pattern_thm]] |
205 end |
205 end |
206 |
206 |
207 val add_nominal_function = |
207 val add_nominal_function = |
208 gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
208 gen_add_nominal_function false Specification.check_spec (Type_Infer.anyT @{sort type}) |
209 fun add_nominal_function_cmd a b c d int = |
209 fun add_nominal_function_cmd a b c d int = |
210 gen_add_nominal_function int Specification.read_spec "_::type" a b c d |
210 gen_add_nominal_function int Specification.read_spec "_::type" a b c d |
211 |
211 |
212 fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy = |
212 fun gen_nominal_function do_print prep default_constraint fixspec eqns config lthy = |
213 let |
213 let |
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 (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 @{sort type}) |
224 fun nominal_function_cmd a b c int = |
224 fun nominal_function_cmd a b c int = |
225 gen_nominal_function int Specification.read_spec "_::type" a b c |
225 gen_nominal_function int Specification.read_spec "_::type" a b c |
226 |
226 |
227 |
227 |
228 fun add_case_cong n thy = |
228 fun add_case_cong n thy = |