equal
deleted
inserted
replaced
657 case trm of |
657 case trm of |
658 Abs (x, T, t) => |
658 Abs (x, T, t) => |
659 let |
659 let |
660 val ty1 = fastype_of trm |
660 val ty1 = fastype_of trm |
661 in |
661 in |
662 (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) (Abs (x, T, t))) |
662 (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm) |
663 end |
663 end |
664 | Const (@{const_name "All"}, ty) $ t => |
664 | Const (@{const_name "All"}, ty) $ t => |
665 let |
665 let |
666 val ty1 = domain_type ty |
666 val ty1 = domain_type ty |
667 val ty2 = domain_type ty1 |
667 val ty2 = domain_type ty1 |
1007 apply (assumption) |
1007 apply (assumption) |
1008 apply (metis) |
1008 apply (metis) |
1009 done |
1009 done |
1010 |
1010 |
1011 ML {* |
1011 ML {* |
1012 fun instantiate_tac thm = (Subgoal.FOCUS (fn {concl, context, ...} => |
1012 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, context, ...} => |
1013 let |
1013 let |
1014 val pat = cterm_of (ProofContext.theory_of context) (concl_of thm) |
1014 val pat = Drule.strip_imp_concl (cprop_of thm) |
1015 val insts = Thm.match (pat, concl) |
1015 val insts = Thm.match (pat, concl) |
1016 in |
1016 in |
1017 rtac (Drule.instantiate insts thm) 1 |
1017 rtac (Drule.instantiate insts thm) 1 |
1018 end)) |
1018 end) |
1019 *} |
1019 *} |
1020 |
1020 |
1021 |
1021 |
1022 |
1022 |
1023 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
1023 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |