#
5417af9d |
|
31-Mar-2020 |
Arve Gengelbach <arve.gengelbach@it.uu.se> |
remove lcsymtacs (github issue #666) The lcsymtacs structure is regarded superseded as it plainly is a shorthand for opening the following modules: Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib Rewrite bossLib Thm_cont
|
#
8ab15c2f |
|
21-May-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Replace a number of delsimps calls with temp_delsimps instead The problem with delsimps is that it makes the change permanent for all descendent theories. Some proofs need adjusting as a result.
|
#
b98f5ead |
|
10-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Be more careful over handling of ThmSetData and rebinding of thm names In particular, it was previously possible to do val thm = store_thm("thm[some_attribute]", tm1, tac2); val thm = store_thm("thm", tm2, tac2); and have the second thm be exported but to pick up the attribute from the first call. This is clearly outrageous, so now the attribute is lost when the second theorem is slotted into the theory. Working through all this found three places where this double-definition pattern was happening (there may yet be more). In src/finite_map and src/list the second theorem was clearly just redundant and could be deleted. The example in fun-op-sem is slightly more interesting: there it defines a function (which definition gives that function a "compute" attribute), and then restates the definition, saving it under the same name ("foo_def"). Though arguably bad style, it's important that the second theorem replace the first, and that it should have the "compute" attribute. Here the change is to explicitly add that attribute to the second theorem. Finally, all this work revealed that Theory.sml's handling of the NewBinding theory-delta hook was wrong and caused changes to be dropped after the hook function was called. Debugging *that* led me to add a pp field to the LoadableThyData registration process so that theory-data values could be inspected more easily. There is also a trace variable to turn on some debugging output in Theory.
|
#
90dc773d |
|
28-Jun-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get fun-op-sem/for to build again Add it to the build sequence
|
#
46d2ac66 |
|
26-Jun-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix Q.GENL to handle variables in same order as GENL. Closes #428
|
#
49d0d7ba |
|
19-Mar-2016 |
Ramana Kumar <ramana@member.fsf.org> |
Fix fun-op-sem example It was broken by changes in abbreviated simplification tactics.
|
#
4d12051c |
|
11-Jan-2016 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
added a comparison with Charguéraud' Pretty Big Step approach Yong Kiam and I did most of the development for this commit.
|
#
8be770c3 |
|
18-Oct-2015 |
Ramana Kumar <ramana@member.fsf.org> |
update fun-op-sem example
|
#
efca65d5 |
|
21-Mar-2015 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
fun-op-sem: improved file structure, more comments
|