equal
deleted
inserted
replaced
347 |
347 |
348 (*version without the hyps argument*) |
348 (*version without the hyps argument*) |
349 fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [] |
349 fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [] |
350 |
350 |
351 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc |
351 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc |
352 fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT) |
352 fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context())) s |
353 val prep_pats = map prep_pat |
353 val prep_pats = map prep_pat |
354 |
354 |
355 fun is_numeral (Const("Numeral.number_of", _) $ w) = true |
355 fun is_numeral (Const("Numeral.number_of", _) $ w) = true |
356 | is_numeral _ = false |
356 | is_numeral _ = false |
357 |
357 |