{"shas":[["e80ad9ed507317733ce72fd864002f023fcf2687","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Get TFL to allow <=> in definitions (of relations or predicates).\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9101 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["57ca7faf0ff19b7b089dbf71389d3354f1f18fb8","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Fix (and test) for bug in quotient package: it was parsing with global grammar.\n\nIt's OK to parse with the global grammar when in a script file as one\nknows then what context one is parsing strings within.  But in library\ncode, such as quotient.sml, it is dangerous to rely on the behaviour\nof the global grammar because users may have changed it to the\nlibrary's disadvantage.  Better to do all of one's internal parsing\nwith a known grammar.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9102 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["ceae08e736f4c7aae12a56c64f428956fe348095","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Prove a varying parameter version of the term recursion principle.\n\nGet termScript to compile with the new principle.\nMore work will be required to adjust remaining lambda-calculus scripts.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9103 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["2cd09801ddcbd8926eccd668b938dacdb1e68c3a","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Rework lambda-theory scripts to use new varying parameter recursion theorem.\n\nAlso make work for myself by having some of the script files use\n'tight' equality.  Later files get switched back to loose (prec = 100)\nequality, because it was all getting to be too much work.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9104 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["6953be76b0251a35bdbcef85c1ab3026d27d5226","9aa6dc5071328caa31d9be472f1bcc300b365475@15ed8c29-5735-0410-93a9-c5146456d060","Improve HolSmt's coverage of bit-vector problems.\n\nThis involves mapping some HOL bit-vector operations into suitable SMT-LIB\noperations.  In particular, provide support for:\n\n1. reduce_and, reduce_or, etc.  This is done using wordsLib.EXPAND_REDUCE_CONV.\n\n2. word_lsb, word_msb, word_bit, word_bits, word_slice and bit_field_insert.\nThis is done through rewrites.\n\n3. (w2w:'a word->'b word) and (sw2sw:'a word->'b word) where the word size\ndecreases.  Again done using rewrites.\n\n4.  ((h >< l) w) : 'a word, where 'a word is larger than h + 1 - l.  This is\ndone using wordsLib.EXTEND_EXTRACT_CONV.\n\n\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9105 15ed8c29-5735-0410-93a9-c5146456d060","acjf3"],["25acabe256bec7a86fba9fbcc066a044d9f54ce9","9aa6dc5071328caa31d9be472f1bcc300b365475@15ed8c29-5735-0410-93a9-c5146456d060","Some extra list theorems.\n\n\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9106 15ed8c29-5735-0410-93a9-c5146456d060","acjf3"],["facd2fa557a3c2236af9359f2d6144f8f05595d9","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Get lambda/typing directory to build again.\n\nHad to deal with termScript stealing the \\rightarrow syntax (I made\nthat theft local to termScript); and with tight equality.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9107 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["7f5619d5f171fe7e9ddd9fb01518824dafdc130e","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Moved prekernel/FinalTheory-sig.sml to be postkernel/Theory.sig.\n\nThis simplifies the core a little.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9108 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["b34430e99d67ed16e245e75a7837a9b81781dac3","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Remove Holmakefile in postkernel (it broke stuff and is now unnecessary)\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9109 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["b3bc3ea471296c78df25bfaea0ddc0aa24042435","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Fix parser used in help so that sigs can contain structure foo : sig .. end\n\nAlso report errors by file.  For the moment, no errors are reported in\nthe system's collected signature files, which is nice.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9110 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["1604d167c9f31cf099e63aff4229c846794ff3c4","c2f29c1fe63a5b140d399725ad67ab88bbfcdf76@15ed8c29-5735-0410-93a9-c5146456d060","Fix src/HolSmt/Library.sml so that it compiles again.\n\nThere is far less 'open' in Library.sml than is typical.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9111 15ed8c29-5735-0410-93a9-c5146456d060","michaeln"],["065f585843c0f7b0550b1b56551581d8d522121a","6d1c99ca2b25be0f02c158a448b4a95336d94c99@15ed8c29-5735-0410-93a9-c5146456d060","Replace new_axiom for Separation_ax with store_thm and a proof.\n\nAs in Obua's HOLZF for Isabelle.\nAlso removed some trailing whitespace.\n\ngit-svn-id: https://hol.svn.sourceforge.net/svnroot/hol/HOL@9112 15ed8c29-5735-0410-93a9-c5146456d060","xrchz"],["6089ad68b54b07ff57c9084574d1452f02f3c453","2ab5dffb42a3e7f72a5da4dda8156124ac6d4d7d@gmail.com","Merge branch 'master' into category","Ramana Kumar"]],"ref":"refs/heads/category","size":13,"head":"6089ad68b54b07ff57c9084574d1452f02f3c453","push_id":33399338}