equal
deleted
inserted
replaced
201 |
201 |
202 ML \<open> |
202 ML \<open> |
203 structure Blast = Blast |
203 structure Blast = Blast |
204 ( |
204 ( |
205 structure Classical = Cla |
205 structure Classical = Cla |
206 val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close> |
206 val Trueprop_const = dest_Const \<^Const>\<open>Trueprop\<close> |
207 val equality_name = \<^const_name>\<open>eq\<close> |
207 val equality_name = \<^const_name>\<open>eq\<close> |
208 val not_name = \<^const_name>\<open>Not\<close> |
208 val not_name = \<^const_name>\<open>Not\<close> |
209 val notE = @{thm notE} |
209 val notE = @{thm notE} |
210 val ccontr = @{thm ccontr} |
210 val ccontr = @{thm ccontr} |
211 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
211 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |