equal
deleted
inserted
replaced
99 in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end |
99 in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end |
100 |
100 |
101 fun prove_conv_nohyps tacs sg = prove_conv tacs sg []; |
101 fun prove_conv_nohyps tacs sg = prove_conv tacs sg []; |
102 |
102 |
103 fun prep_simproc (name, pats, proc) = |
103 fun prep_simproc (name, pats, proc) = |
104 Simplifier.simproc (Theory.sign_of (the_context())) name pats proc; |
104 Simplifier.simproc (the_context()) name pats proc; |
105 |
105 |
106 fun is_numeral (Const("Numeral.number_of", _) $ w) = true |
106 fun is_numeral (Const("Numeral.number_of", _) $ w) = true |
107 | is_numeral _ = false |
107 | is_numeral _ = false |
108 |
108 |
109 fun simplify_meta_eq f_number_of_eq f_eq = |
109 fun simplify_meta_eq f_number_of_eq f_eq = |