equal
deleted
inserted
replaced
113 (* split theorem thm_1 & ... & thm_n into n theorems *) |
113 (* split theorem thm_1 & ... & thm_n into n theorems *) |
114 |
114 |
115 fun split_conj_thm th = |
115 fun split_conj_thm th = |
116 ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th]; |
116 ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th]; |
117 |
117 |
118 val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj}); |
118 val mk_conj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>); |
119 val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj}); |
119 val mk_disj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.disj\<close>); |
120 |
120 |
121 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0)); |
121 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0)); |
122 |
122 |
123 |
123 |
124 (* instantiate induction rule *) |
124 (* instantiate induction rule *) |