changeset 20217 | 25b068a99d2b |
parent 20070 | 3f31fb81b83a |
child 20872 | 528054ca23e3 |
20216:f30b73385060 | 20217:25b068a99d2b |
---|---|
164 Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover; |
164 Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover; |
165 |
165 |
166 end; |
166 end; |
167 |
167 |
168 |
168 |
169 |
|
170 |
|
171 (*** Simproc for Let ***) |
169 (*** Simproc for Let ***) |
172 |
170 |
173 val use_let_simproc = ref true; |
171 val use_let_simproc = ref true; |
174 |
172 |
175 local |
173 local |