347 |
347 |
348 (** realizability predicate **) |
348 (** realizability predicate **) |
349 |
349 |
350 val (ind_info, thy3') = thy2 |> |
350 val (ind_info, thy3') = thy2 |> |
351 InductivePackage.add_inductive_global (serial_string ()) |
351 InductivePackage.add_inductive_global (serial_string ()) |
352 {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty, |
352 {quiet_mode = false, verbose = false, kind = Thm.generated_theoremK, alt_name = Binding.empty, |
353 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
353 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
354 rlzpreds rlzparams (map (fn (rintr, intr) => |
354 rlzpreds rlzparams (map (fn (rintr, intr) => |
355 ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), |
355 ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), |
356 subst_atomic rlzpreds' (Logic.unvarify rintr))) |
356 subst_atomic rlzpreds' (Logic.unvarify rintr))) |
357 (rintrs ~~ maps snd rss)) [] ||> |
357 (rintrs ~~ maps snd rss)) [] ||> |