#
0801c6f2 |
|
12-Oct-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Simplify grammar handling by using abstract ancestral data framework This is not fully worked out yet, and the abstract framework has only been instantiated on the one test-case. It's definitely worth it there though as there can be less awful code smashed into fooTheory.sml files as a result. Aim is to instantiate theorem-sets in the same way though so that it will be possible to access srw_ss() as it was at different points in the theory hierarchy. Not yet clear if AncestryData should be responsible for holding onto the underlying references that hold the global "values" (grammars, simpsets, etc). Changes in examples fix various adjoin calls that either shouldn't be there at all (TypeBase now has export; or need to be made "after completion" so that parses work correctly (these should be using exportable data themselves)).
|
#
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
|
#
2f73a671 |
|
18-Feb-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Clean labelledTermsScript to use simp-attribute and nice quotes
|
#
698d4c1b |
|
04-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix examples/lambda/barendregt for tight equality
|
#
18934f7c |
|
03-Dec-2018 |
Johannes Åman Pohjola <johannes.amanpohjola@data61.csiro.au> |
Reconcile store_thms with diverging names in db and val binding
|
#
0466cdbc |
|
25-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix some adjoin calls in examples/lambda
|
#
732b9f9e |
|
04-May-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extra parameter for new_type command in nomdatatype allowing for multi-types. Doesn't work unless each 'type' allows a 'VAR' constructor, which is not the case in first order formulas and terms, for example.
|
#
bc294d17 |
|
02-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extract a usable half-way point from nominal_datatype branch. This replaces the is_perm predicate with a type embodying that predicate. It doesn't include the subsequent work on allowing multiple 'atom' types.
|
#
25da727d |
|
24-Jul-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Terms and labelled terms now derived from generic terms. This is a big change that points to the implementation of a complete nominal datatype package. The use of generic terms means that we only need to do one hairy quotient, and one hairy derivation of a recursion principle. The recursion principle in question features a new "FCB" (one of the side-conditions that need to be proved in order to get a recursive function admitted). Though I think it's better, it can be a little fiddlier to prove. It's also stronger, so in theory, there may be reasonable functions that the new FCB rejects. It should certainly be possible to automate the bulk of the new fiddly proofs.
|
#
0bbd2a7e |
|
21-Jun-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix. 90+% of this work was done by Ramana Kumar. The following list are the commits for a series of individual commits that have been squished into one big change: * remove mention of TruePrefix from the add_rule docfile * first batch of changes removing TruePrefix from src/parse * replace TruePrefix by Prefix in boolScript.sml * remove TruePrefix from Rsyntax is a fixity ever required for new_specification? * some more Prefix -> NONE and TruePrefix -> Prefix in theories * TruePrefix changes for datatype * TruePrefix changes for res_quan * TruePrefix->Prefix in a TeX selftest * TruePrefix changes for quotient * TruePrefix changes for integer and real * fix quotient examples for TruePrefix removal * more fixes for quotient examples * fixes for lambda example for TruePrefix removal * Reword description manual in light of removal of TruePrefix. * Fix msgTheory quotient example; Poly 5.3 had problems with monotypes. * Fixes for files in examples/lambda given removal of TruePrefix. * Fix in examples/unification given removal of TruePrefix. * Fix in examples/HolCheck given removal of TruePrefix. * Fixes in examples/acl2 given removal of TruePrefix.
|
#
4164a076 |
|
15-Oct-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Revise the base theory of nominal sets to make much greater use of overloading, thereby reduce the number of Define-d constants. This reduces the number of theorems as well. With some theorems disappearing, there were a few knock-on effects in descendent theories.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
fa39b570 |
|
02-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement a FRESH_TAC that freshens bound variables throughout a term.
|
#
e3d9c2ec |
|
02-Mar-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Recast binderLib's internal databases about "binder"-information for types. In the process, give up on the attempt to make this technology work for the "old" style of recursion theorem as in my TPHOLs paper. Now the only style supported is the quotient + nominal proof (which is what is in barendregt).
|
#
5d35f46c |
|
24-Feb-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
When loaded interactively, labelledTermsTheory produced an "overloading has multiple resolutions" error. This was caused by the script "adjoining" something to the theory with an ambiguous parse in it.
|
#
176a481a |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixes for these examples, and an updated MANIFEST/README in other-models. The other-models directory had become particularly stale. I obviously need to check that it works more often. (Main problem: change to behaviour of Q.INST.)
|
#
b541f3ea |
|
26-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Proofs and tools broke when I changed the behaviour of parse_in_context. Thanks for Peter for alerting me to the problem (should be running build -selftest more often myself). (Also make barendregt directory QUIT_ON_FAILURE, and removed a duplicate proof in finite_developments.)
|
#
effc431b |
|
01-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Change export_rewrites back to its old API (without requiring an extra string). When exported, the resulting simpset fragment always picked up the name of the theory to be the base of its name, so there didn't seem much point in giving users a false impression of naming power.
|
#
aed05f4e |
|
20-Jul-2008 |
Konrad Slind <konrad.slind@gmail.com> |
A whole mess of small changes intended at making simpsets prettyprint informatively in the interactive loop. Very possibly I haven't updated all the files in the examples directories.
|
#
7cf5c42f |
|
09-Jul-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Completely reorganise these files into some sensible directories. Also, add a file demonstrating that the McKinna-Pollack two-sorted raw syntax does indeed behave properly (links appropriately to beta over quotiented terms).
|