equal
deleted
inserted
replaced
90 |
90 |
91 val arith_special = thms"arith_special"; |
91 val arith_special = thms"arith_special"; |
92 |
92 |
93 structure Bin_Simprocs = |
93 structure Bin_Simprocs = |
94 struct |
94 struct |
95 fun prove_conv tacs sg (hyps: thm list) xs (t, u) = |
95 fun prove_conv tacs ctxt (_: thm list) (t, u) = |
96 if t aconv u then NONE |
96 if t aconv u then NONE |
97 else |
97 else |
98 let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) |
98 let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) |
99 in SOME (Goal.prove sg xs [] 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 fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] []; |
|
103 |
102 |
104 fun prep_simproc (name, pats, proc) = |
103 fun prep_simproc (name, pats, proc) = |
105 Simplifier.simproc (Theory.sign_of (the_context())) name pats proc; |
104 Simplifier.simproc (Theory.sign_of (the_context())) name pats proc; |
106 |
105 |
107 fun is_numeral (Const("Numeral.number_of", _) $ w) = true |
106 fun is_numeral (Const("Numeral.number_of", _) $ w) = true |