equal
deleted
inserted
replaced
77 handle TERM _ => NONE |
77 handle TERM _ => NONE |
78 end*} |
78 end*} |
79 |
79 |
80 text {* The setup for the simproc is *} |
80 text {* The setup for the simproc is *} |
81 |
81 |
82 simproc_setup add_sp ("t1 + t2") = {* K add_sp_aux *} |
82 simproc_setup %gray add_sp ("t1 + t2") = {* K add_sp_aux *} |
83 |
83 |
84 text {* and a test case is the lemma *} |
84 text {* and a test case is the lemma *} |
85 |
85 |
86 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
86 lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" |
87 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *}) |
87 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *}) |