equal
deleted
inserted
replaced
122 |
122 |
123 val refl_tac = resolve_tac refl_thms; |
123 val refl_tac = resolve_tac refl_thms; |
124 |
124 |
125 fun find_res thms thm = |
125 fun find_res thms thm = |
126 let fun find [] = (prths thms; error"Check Simp_Data") |
126 let fun find [] = (prths thms; error"Check Simp_Data") |
127 | find(th::thms) = thm RS th handle _ => find thms |
127 | find(th::thms) = thm RS th handle THM _ => find thms |
128 in find thms end; |
128 in find thms end; |
129 |
129 |
130 val mk_trans = find_res trans_thms; |
130 val mk_trans = find_res trans_thms; |
131 |
131 |
132 fun mk_trans2 thm = |
132 fun mk_trans2 thm = |
133 let fun mk[] = error"Check transitivity" |
133 let fun mk[] = error"Check transitivity" |
134 | mk(t::ts) = (thm RSN (2,t)) handle _ => mk ts |
134 | mk(t::ts) = (thm RSN (2,t)) handle THM _ => mk ts |
135 in mk trans_thms end; |
135 in mk trans_thms end; |
136 |
136 |
137 (*Applies tactic and returns the first resulting state, FAILS if none!*) |
137 (*Applies tactic and returns the first resulting state, FAILS if none!*) |
138 fun one_result(tac,thm) = case Seq.pull(tac thm) of |
138 fun one_result(tac,thm) = case Seq.pull(tac thm) of |
139 Some(thm',_) => thm' |
139 Some(thm',_) => thm' |