equal
deleted
inserted
replaced
506 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
506 val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3; |
507 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
507 fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp)) |
508 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
508 val lthy22 = Class.prove_instantiation_instance tac lthy21 |
509 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
509 val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos; |
510 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
510 val (names, supp_eq_t) = supp_eq fv_alpha_all; |
511 (* val _ = warning "Support Equations"; |
511 val _ = warning "Support Equations"; |
512 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => []; |
512 (*supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1*) |
513 val lthy23 = note_suffix "supp" q_supp lthy22;*) |
513 val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => Skip_Proof.cheat_tac thy)) handle _ => []; |
514 in |
514 val lthy23 = note_suffix "supp" q_supp lthy22; |
515 (0, lthy22) |
515 in |
|
516 (0, lthy23) |
516 end |
517 end |
517 *} |
518 *} |
518 |
519 |
519 section {* Preparing and parsing of the specification *} |
520 section {* Preparing and parsing of the specification *} |
520 |
521 |