{"shas":[["30f846625621bc0ced3928389dab38823b448068","4d3586b959590a6e034649b5cc7435fb7d9ba30c@cs.pdx.edu","fix proof script to make halicore_data work for types without parameters","Brian Huffman"],["e342a0037ae221121457b3a344d3c551fc10fa9c","4d3586b959590a6e034649b5cc7435fb7d9ba30c@cs.pdx.edu","new file Halicore_Prelude.thy, with definition and syntax for list datatype","Brian Huffman"],["f1dfafa8339066acc20ebe150bf59d78bb8a93f1","4d3586b959590a6e034649b5cc7435fb7d9ba30c@cs.pdx.edu","halicore_fun command now proves and registers typing rules for new functions","Brian Huffman"],["a6f5a8c7ab449719499d26a176da11f127ed9b2f","4d3586b959590a6e034649b5cc7435fb7d9ba30c@cs.pdx.edu","Examples.thy: update definitions to use the halicore_fun command","Brian Huffman"],["11c3bc05a971627cb03cdca4120ad23352a7fb39","4d3586b959590a6e034649b5cc7435fb7d9ba30c@cs.pdx.edu","function.ML: use TRYALL tactical, which should produce better error messages","Brian Huffman"],["cd0f777c61439b33c125d768733c998e0d3412a7","be6b7294d0ec315b391da6f4a69819010cef0e52@galois.com","Merge branch 'master' of github.com:atomb/core-to-isabelle into rewrite-translator","Jason Dagit"]],"ref":"refs/heads/rewrite-translator","size":6,"head":"cd0f777c61439b33c125d768733c998e0d3412a7","push_id":40861864}