equal
deleted
inserted
replaced
118 (* split theorem thm_1 & ... & thm_n into n theorems *) |
118 (* split theorem thm_1 & ... & thm_n into n theorems *) |
119 |
119 |
120 fun split_conj_thm th = |
120 fun split_conj_thm th = |
121 ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th]; |
121 ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th]; |
122 |
122 |
123 val mk_conj = foldr1 (HOLogic.mk_binop "op &"); |
123 val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"}); |
124 val mk_disj = foldr1 (HOLogic.mk_binop "op |"); |
124 val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"}); |
125 |
125 |
126 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0)); |
126 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0)); |
127 |
127 |
128 |
128 |
129 (* instantiate induction rule *) |
129 (* instantiate induction rule *) |