equal
deleted
inserted
replaced
53 val prove_termination: Proof.context -> Function.info * local_theory |
53 val prove_termination: Proof.context -> Function.info * local_theory |
54 |
54 |
55 (* transformations of premises in inductions *) |
55 (* transformations of premises in inductions *) |
56 val transform_prem1: Proof.context -> string list -> thm -> thm |
56 val transform_prem1: Proof.context -> string list -> thm -> thm |
57 val transform_prem2: Proof.context -> string list -> thm -> thm |
57 val transform_prem2: Proof.context -> string list -> thm -> thm |
|
58 |
|
59 (* transformation into the object logic *) |
|
60 val atomize: thm -> thm |
58 end |
61 end |
59 |
62 |
60 |
63 |
61 structure Nominal_Library: NOMINAL_LIBRARY = |
64 structure Nominal_Library: NOMINAL_LIBRARY = |
62 struct |
65 struct |
254 |
257 |
255 fun transform_prem2 ctxt names thm = |
258 fun transform_prem2 ctxt names thm = |
256 map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm |
259 map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm |
257 |
260 |
258 |
261 |
|
262 (* transformes a theorem into one of the object logic *) |
|
263 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars |
|
264 |
259 |
265 |
260 end (* structure *) |
266 end (* structure *) |
261 |
267 |
262 open Nominal_Library; |
268 open Nominal_Library; |