{"shas":[["7ccc0eee42382cfa19b9fae1865b668114c939e0","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Terms and labelled terms now derived from generic terms.\n\nThis is a big change that points to the implementation of a complete\nnominal datatype package.  The use of generic terms means that we only\nneed to do one hairy quotient, and one hairy derivation of a recursion\nprinciple.\n\nThe recursion principle in question features a new \"FCB\" (one of the\nside-conditions that need to be proved in order to get a recursive\nfunction admitted).  Though I think it's better, it can be a little\nfiddlier to prove.  It's also stronger, so in theory, there may be\nreasonable functions that the new FCB rejects. It should certainly be\npossible to automate the bulk of the new fiddly proofs.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9163 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["5350ce08304609eca1ae41da55e5e5b8d06e6ec7","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Revised Barendregt Chapter 11.1 theory\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9164 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["c91039a35146abc637c43c1507538a903c8b04b1","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Fixed finite_developments; it's more robust than it was now.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9165 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["0bc5c27d7187d7a32b4e7e3af9ed641aae5dba52","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Fixed standardisation script (all of barendregt directory builds).\n\nIssue here was that new theorems pick slightly different variable\nnames in some places, and this causes breakage.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9166 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["ebd24aa4799cdbaae46353d4485f8b53522958e1","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Other models build with new FCB.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9167 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["288e4990488c990c0250b992531673d216dbabd8","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Get computability theories to build with new labelled terms.\n\n(Issue was that there is no FV constant in that theory anymore, just an\noverload to supp ltpm.)\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9168 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"]],"ref":"refs/heads/master","size":6,"head":"288e4990488c990c0250b992531673d216dbabd8","push_id":37469733}