Commits

Breadcrumbs

History for

onf6e646d

User selector

All users

Datepicker

All time

Commit History

Commits on May 28, 2020

• Product measure and Tonelli's theorem

  

  binghe

  authored and

  Michael Norrish

  committed
  c0ca1d1

Commits on May 21, 2020

• Merge branch 'develop' into probability_doc

  

  Michael Norrish

  authored
  4278783

Commits on May 6, 2020

• Release notes for list+rich_list theory changes

  

  AndreasLoow

  authored and

  Michael Norrish

  committed
  ce5f9d5

Commits on Apr 12, 2020

• Note the removal of rich_listTheory.REVERSE in release notes (Incompatibilities); all -t2 tests passed.

  binghe

  committed
  8ef8378

Commits on Apr 11, 2020

• Updated HOL Description for mathematical theories (with other cumulative fixes)

  binghe

  committed
  486e965

Commits on Dec 18, 2019

• Holwrap (HOL-Theorem-Prover#758)

  Show description for 505150c
  

  lxndrcx

  authored and

  Michael Norrish

  committed
  505150c

Commits on Nov 13, 2019

• Minor typo/grammar corrections in release notes

  mn200

  committed
  d131fb2

Commits on Nov 10, 2019

• AKS mechanisation (HOL-Theorem-Prover#750)

  Show description for b3b2a8f
  

  jhlchan

  authored and

  Michael Norrish

  committed
  b3b2a8f

Commits on Oct 27, 2019

• Added derivativeTheory and integrationTheory into release notes

  

  binghe

  authored and

  Michael Norrish

  committed
  3a67620

Commits on Sep 27, 2019

• Correct typo in release notes

  mn200

  committed
  6c4b054

Commits on Sep 20, 2019

• The new HOL-Probability based on [0,+Inf]-measure theory (HOL-Theorem-Prover#735)

  Show description for c4db120
  

  binghe

  authored and

  Michael Norrish

  committed
  c4db120

Commits on Aug 27, 2019

• Add special Overload syntax to map to overload_on

  Show description for c8feb43
  mn200

  committed
  c8feb43

Commits on Aug 26, 2019

• Allow "local" attribute to be added to Type syntax

  Show description for 70744e4
  mn200

  committed
  70744e4

Commits on Aug 19, 2019

• Update tags to label release as Kananaskis-13

  mn200

  committed
  b69d328

• Document Triviality and local attribute for Theorem

  mn200

  committed
  8d9ca0d

Commits on Aug 18, 2019

• Tactic to automate some routine set theory by reduction to FOL (HOL-Theorem-Prover#722)

  Show description for 3587911
  

  binghe

  authored and

  Michael Norrish

  committed
  3587911

Commits on Aug 16, 2019

• Further document drule breakage by linking to CakeML's old_drule

  mn200

  committed
  8cc876e

Commits on Aug 12, 2019

• release notes: italicise REFERENCE and DESCRIPTION

  Show description for 577138e
  mn200

  committed
  577138e

• release notes: describe drule incompatibility & fix more accurately

  mn200

  committed
  2dd68e1

Commits on Aug 11, 2019

• Document drule change from 812a08a

  mn200

  committed
  9cb0910

Commits on Aug 9, 2019

• Document new Datatype and Type syntaxes

  mn200

  committed
  2645ca2

Commits on Aug 8, 2019

• Merge pull request HOL-Theorem-Prover#720 from binghe/bisimulationTheory

  Show description for 69de791
  

  Michael Norrish

  authored
  69de791

• Fixed wrong spelling of names, sorry.

  binghe

  committed
  2878b09

• Moved BISIM(_REL) theorems to bisimulationTheory with coinduction principles added

  binghe

  committed
  2737e79

• Mention compactness example in release notes

  Show description for fe603ee
  mn200

  committed
  fe603ee

Commits on Aug 5, 2019

• Mention incompatibility of foo_def_compute turning into foo_compute

  Show description for dc55941
  mn200

  committed
  dc55941

Commits on Jul 31, 2019

• Extend and move theory of lists-of-nats encoded as nats

  Show description for 5567268
  mn200

  committed
  5567268

Commits on Jul 22, 2019

• Implement INST_TYPE facility within Q.SPEC_THEN

  Show description for 82d2257
  mn200

  committed
  82d2257

• Add CoInductive syntax (mirroring Inductive syntax)

  Show description for bb0a5ef
  mn200

  committed
  bb0a5ef

• Document new Inductive syntax in release notes

  mn200

  committed
  cec2050

Commits on Jul 11, 2019

• bug fixed + new tools

  

  Thibault Gauthier

  committed
  3ae700f

Commits on Jul 8, 2019

• Announce add_strliteral_form in release notes

  mn200

  committed
  8a1dd56

Commits on Jul 1, 2019

• Clean up MEM_DROP situation

  Show description for 8877f97
  mn200

  committed
  8877f97

Commits on Jun 20, 2019

• Move DEFAULT_TARGETS write-up to new features part of release notes

  Show description for 495b865
  mn200

  committed
  495b865

Commits on May 23, 2019

• Merge branch 'develop' into tightequality

  mn200

  committed
  c779826

Pagination

Previous

Next