Michael Norrish
mn200

Organizations

@HOL-Theorem-Prover
Jul 12, 2016
@mn200
  • @mn200 2960d84
    Show that the Cont(inuation) monad is possible
Jul 11, 2016
@mn200
  • @mn200 b4b73a3
    Parse & convert type annotations on exps and pats
Jul 3, 2016
@mn200
Jul 3, 2016
@mn200
  • @mn200 4682f57
    Move patternMatchesExample to .ML suffix
Jun 29, 2016
@mn200
Jun 29, 2016
@mn200
Jun 29, 2016
@mn200
Report line numbers associated with (non-parsing) HOL_ERRs
Jun 29, 2016
@mn200
Jun 28, 2016
@mn200
  • @mn200 ed192c9
    Strengthen statement of TAKE_SUM
Jun 28, 2016
@mn200
listTheory.TAKE_SUM has an unnecessary precondition
Jun 27, 2016
@mn200
Jun 27, 2016
mn200 merged pull request HOL-Theorem-Prover/HOL#353
@mn200
User config changes (for ANSI colors)
2 commits with 31 additions and 10 deletions
Jun 27, 2016
@mn200
  • @mn200 dc6f554
    Remove last cheat in clos_to_bvlProof
Jun 26, 2016
@mn200
Jun 26, 2016
@mn200
  • @mn200 d8353b0
    Push syntactic expr. preconds through renumber in clos_to_bvl
Jun 26, 2016
@mn200
  • @mn200 ccb9041
    Push esgc_free through intro_multi in clos_to_bvl
Jun 25, 2016
@mn200
  • @mn200 b18690a
    Add two preconds for known that pat_to_clos needs to establish
Jun 24, 2016
@mn200
  • @mn200 bbfd28f
    Work around a minor overloading bug in HOL
Jun 24, 2016
@mn200
Jun 24, 2016
@mn200
  • @mn200 1e50d43
    Rename constants in clos_knownProofs
Jun 24, 2016
@mn200
  • @mn200 7e49980
    Really fix names in regexpScript
mn200 deleted branch bvl_to_clos-opt at CakeML/cakeml
Jun 24, 2016
Jun 24, 2016
@mn200
Jun 23, 2016
@mn200
  • @mn200 d44ce43
    Force reg_alloc .uo file to mention lprefix_lub correctly
Jun 23, 2016
@mn200
Jun 23, 2016
@mn200
  • @mn200 75b3425
    Be more explicit with variable names to fix expk breakage
Jun 23, 2016
@mn200
  • @mn200 d15b7d7
    Move material from clos_knownProofs to closProps
Jun 23, 2016
@mn200
  • @mn200 e3d390e
    Fix regexpScript's line-endings and trailing whitespace
mn200 created branch bvl_to_clos-opt at CakeML/cakeml
Jun 23, 2016
Jun 22, 2016
@mn200
  • @mn200 239414f
    Fix compilerComputeLib.sml given 39dcbfb