equal
deleted
inserted
replaced
1987 ML{*fun get_thm_alt ctxt (t, n) = |
1987 ML{*fun get_thm_alt ctxt (t, n) = |
1988 let |
1988 let |
1989 val num = HOLogic.mk_number @{typ "nat"} n |
1989 val num = HOLogic.mk_number @{typ "nat"} n |
1990 val goal = Logic.mk_equals (t, num) |
1990 val goal = Logic.mk_equals (t, num) |
1991 val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @ |
1991 val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @ |
1992 @{thms nat_number} @ @{thms neg_simps} @ @{thms plus_nat.simps} |
1992 @{thms eval_nat_numeral} @ @{thms neg_simps} @ @{thms plus_nat.simps} |
1993 in |
1993 in |
1994 Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1)) |
1994 Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1)) |
1995 end*} |
1995 end*} |
1996 |
1996 |
1997 text {* |
1997 text {* |