Commits

Branch selector

 a9a7e76

User selector

All users

Datepicker

All time

Commit History

Commits on Jun 15, 2020

• Define an adjacent relation on lists and their elements

  Show description for a9a7e76
  

  Michael Norrish

  committed
  a9a7e76

• Provide default inductions for TC, RTC, and EQC

  Show description for 8e5ab83
  

  Michael Norrish

  committed
  8e5ab83

• Fix bug preventing induction on negated relation

  Show description for b5ca4a1
  

  Michael Norrish

  committed
  b5ca4a1

• Delete some unused code in listScript.sml

  

  Michael Norrish

  committed
  68e43f5

Commits on Jun 13, 2020

• Update src for strip_binop change

  

  myreen

  authored and

  Michael Norrish

  committed
  511e4a4

• Update examples for strip_binop change

  

  myreen

  authored and

  Michael Norrish

  committed
  b36433f

• Rename strip_binop -> strip_binop_opt; define strip_binop

  

  myreen

  authored and

  Michael Norrish

  committed
  ab8108a

Commits on Jun 12, 2020

• Remove some trailing whitespace in DESCRIPTION

  

  Michael Norrish

  committed
  8e963a8

• Document new <<- (mlet) syntax in DESCRIPTION and release notes

  

  Michael Norrish

  committed
  01704bc

• Give paragraph-leading quotations more prominence in H. Math section

  

  Michael Norrish

  committed
  15c8093

• Correct misspelling of Chebyshev

  

  Michael Norrish

  committed
  40e73d3

• Give → a LaTeX realisation in the polyscripter umap file

  

  Michael Norrish

  committed
  204149b

• Remove some Unicode in LaTeX files

  

  Michael Norrish

  committed
  1eeca43

• Tidy up DESCRIPTION bibliography

  Show description for 991b3a3
  

  Michael Norrish

  committed
  991b3a3

• Remove bad/stale comment in theories.stex

  

  Michael Norrish

  committed
  3fe7d26

• Unit tests for monadic let syntax

  

  hrutvik

  authored and

  Michael Norrish

  committed
  8d1a2ce

• Add monadic let syntax to monadsyntax

  Show description for da74731
  

  hrutvik

  authored and

  Michael Norrish

  committed
  da74731

• Cleanup of append thms for SORTED

  

  AndreasLoow

  authored and

  Michael Norrish

  committed
  805c501

• emacs-mode: fix font-locking of SML keywords (open, val, etc.)

  

  Michael Norrish

  committed
  06a50fb

• emacs-mode: fix hol-mode's handling of open_...

  Show description for 3ec1bb9
  

  Michael Norrish

  committed
  3ec1bb9

• Fix Unicode problem in 827420b

  

  Michael Norrish

  committed
  b8db52a

Commits on Jun 5, 2020

• Make some minor manual tweaks

  

  Michael Norrish

  committed
  4aff68a

• Implement line-truncation facility for polyscripter

  Show description for 8190bd3
  

  Michael Norrish

  committed
  8190bd3

Commits on Jun 3, 2020

• Add a couple of (automatic) rewrites about OPTION_MAP and OPTREL

  

  Michael Norrish

  committed
  827420b

• Make a bunch of rewrites about relation$inv automatic

  

  Michael Norrish

  committed
  92366ac

• emacs-mode: make regexp searching case-sensitive; SOME not a q'fier

  Show description for ac74972
  

  Michael Norrish

  committed
  ac74972

• emacs-mode: don't make _ a word character in syntax tables

  Show description for 02320b7
  

  Michael Norrish

  committed
  02320b7

Commits on May 29, 2020

• emacs-mode: Allow _ to be "symbol" or "word" in Emacs syntax tables

  Show description for 589e573
  

  Michael Norrish

  committed
  589e573

• emacs-mode: make holscript-debugging-messages-p easier to change

  Show description for b310488
  

  Michael Norrish

  committed
  b310488

• emacs-mode: fix another let-indentation issue

  Show description for 9f019dc
  

  Michael Norrish

  committed
  9f019dc

• Fix breakages caused by 486e965, 508f79e and 8ab15c2

  

  Michael Norrish

  committed
  e47e146

Commits on May 28, 2020

• Product measure and Tonelli's theorem

  

  binghe

  authored and

  Michael Norrish

  committed
  c0ca1d1

• Fix proof broken by 508f79e and 8ab15c2

  

  Michael Norrish

  committed
  0bb1018

Commits on May 27, 2020

• Use new resolve_then to do irule under existential via "INTRO"

  Show description for fbb18a9
  

  Michael Norrish

  committed
  fbb18a9

• Tweak 'using' to now handle unnamed monomorphic theorem arguments

  

  Michael Norrish

  committed
  e99f87f

Pagination

Previous

Next