Permalink
Commits on May 2, 2012
  1. add simp rule for case expressions on lambdas

    Brian Huffman committed May 2, 2012
Commits on Apr 30, 2012
  1. simprocs for comparisons and case expressions can now prove inequalit…

    …ies of constructor tags
    Brian Huffman committed Apr 30, 2012
  2. add simp rules for case expressions

    Brian Huffman committed Apr 30, 2012
  3. hide duplicate constant names from the HOL library

    Brian Huffman committed Apr 30, 2012
Commits on Apr 29, 2012
  1. update comment documenting halicore_fun

    Brian Huffman committed Apr 29, 2012
  2. add definition for constant 'undefined'

    Brian Huffman committed Apr 29, 2012
  3. declare more simp rules

    Brian Huffman committed Apr 29, 2012
Commits on Oct 15, 2011
  1. Halicore_Terms.thy: new theory with hybrid syntactic/denotational model;

    Eventually this will replace the current Halicore_Defs.thy.
    Brian Huffman committed Oct 15, 2011
  2. Halicore_Type_Meaning.thy: completely revised and updated

    Brian Huffman committed Oct 15, 2011
  3. fix incorrect Isabelle2011-1 adaptation: install typecheck as global …

    …solver
    Brian Huffman committed Oct 15, 2011
  4. Defl_Lib.thy: add deflation combinator for dependent strict function …

    …space
    Brian Huffman committed Oct 15, 2011
  5. move some theorems

    Brian Huffman committed Oct 15, 2011
  6. adapt theory files to Isabelle2011-1

    Brian Huffman committed Oct 15, 2011
Commits on Oct 13, 2011
  1. Halicore_Type_Deep.thy: fix broken comment

    Brian Huffman committed Oct 13, 2011
  2. Halicore_Type_Deep.thy: combine TyRec and TyFix into one parameterize…

    …d constructor
    Brian Huffman committed Oct 13, 2011
Commits on Oct 3, 2011
  1. Halicore_Kind.thy: proof automation for kcont predicate

    Brian Huffman committed Oct 3, 2011
  2. Halicore_Type_Deep.thy: tuned some proofs

    Brian Huffman committed Oct 3, 2011
Commits on Aug 27, 2011
  1. rename core2isa to hcr2thy

    dagit committed Aug 27, 2011
  2. add a swapped type example

    dagit committed Aug 27, 2011
Commits on Aug 22, 2011