Commits

Branch selector

 develop

User selector

All users

Datepicker

All time

Commit History

Commits on May 1, 2020

• Enhanced fcpTheory (FCP_FST, FCP_SND, FCP_CONCAT_THM, ...); moved duplicated HAS_SIZE to upstream

  

  binghe

  authored and

  Michael Norrish

  committed
  b8cf66f

  Copy full SHA for b8cf66f

Commits on Apr 30, 2020

• emacs-mode: make parsing better aware of inner HOL syntax

  Show description for 45664ab
  

  Michael Norrish

  committed
  45664ab

  Copy full SHA for 45664ab

Commits on Apr 16, 2020

• Remove redundant compute annotation

  

  HeikoBecker

  authored and

  Michael Norrish

  committed
  e2d0faf

  Copy full SHA for e2d0faf

• Move [compute] annotation for subspt to right place

  

  HeikoBecker

  authored and

  Michael Norrish

  committed
  3c9809b

  Copy full SHA for 3c9809b

Commits on Apr 15, 2020

• Ensure default targets built w/opentheory kernel in res_quan/src

  

  Michael Norrish

  committed
  f311450

  Copy full SHA for f311450

Commits on Apr 14, 2020

• Implement, document and regression-test some "term tactics"

  

  Michael Norrish

  committed
  ef343a1

  Copy full SHA for ef343a1

• Provide inv_img_eq to map equality functions from 1 type to another

  Show description for fdd482a
  

  Michael Norrish

  committed
  fdd482a

  Copy full SHA for fdd482a

• Provide new term-based version of Cases_on

  Show description for a92fc14
  

  Michael Norrish

  committed
  a92fc14

  Copy full SHA for a92fc14

Commits on Apr 13, 2020

• Added hyperlinks and sections (based on initial letters) in HOL REFERENCE

  

  binghe

  authored and

  Michael Norrish

  committed
  99017a8

  Copy full SHA for 99017a8

Commits on Apr 9, 2020

• Merge remote-tracking branch 'origin/develop' into thibault-wip

  

  Thibault Gauthier

  committed
  a8a5e38

  Copy full SHA for a8a5e38

• removing trailing white spaces

  

  Thibault Gauthier

  committed
  49cfb5a

  Copy full SHA for 49cfb5a

• adding Readme to AI_develop

  

  Thibault Gauthier

  committed
  b019822

  Copy full SHA for b019822

• handle HOL_ERR

  

  Thibault Gauthier

  committed
  5dcab5e

  Copy full SHA for 5dcab5e

• fixing tactictoe export + checking if an expression is a theorem from its type in the namespace

  

  Thibault Gauthier

  committed
  42d94f2

  Copy full SHA for 42d94f2

Commits on Apr 8, 2020

• tactictoe: revealing missing data when a file is empty

  

  Thibault Gauthier

  committed
  2ca2505

  Copy full SHA for 2ca2505

• updating infixity + README for tactictoe

  

  Thibault Gauthier

  committed
  7f992e8

  Copy full SHA for 7f992e8

Commits on Apr 6, 2020

• Move the match_position datatype from mp_then to its own file

  Show description for 03829d8
  

  Michael Norrish

  committed
  03829d8

  Copy full SHA for 03829d8

• Move mp_then.PART_MATCH' to Drule and document it

  

  Michael Norrish

  committed
  38092a1

  Copy full SHA for 38092a1

• Support Unicode propositional connectives in .doc files

  

  Michael Norrish

  committed
  b106827

  Copy full SHA for b106827

• Support Unicode gamma (γ) in .doc files

  

  Michael Norrish

  committed
  68eba82

  Copy full SHA for 68eba82

• Move some unification related functions out of transfer into src/1

  Show description for 0bf23cd
  

  Michael Norrish

  committed
  0bf23cd

  Copy full SHA for 0bf23cd

• Fixed building of various HOL OpenTheory packages

  

  binghe

  authored and

  Michael Norrish

  committed
  91ac94f

  Copy full SHA for 91ac94f

Commits on Mar 30, 2020

• faster training + slower search

  

  Thibault Gauthier

  committed
  545a122

  Copy full SHA for 545a122

• changing number of cores

  

  Thibault Gauthier

  committed
  9b51e52

  Copy full SHA for 9b51e52

• premise selection through reinforcement learning on sat theorem proving (first version)

  

  Thibault Gauthier

  committed
  f29e755

  Copy full SHA for f29e755

• simplifying targetd

  

  Thibault Gauthier

  committed
  c8abd58

  Copy full SHA for c8abd58

• allowing to evaluate end states to a value different than 0.0 or 1.0

  

  Thibault Gauthier

  committed
  87fcd83

  Copy full SHA for 87fcd83

Commits on Mar 27, 2020

• continuous rewards for MCTS

  

  Thibault Gauthier

  committed
  d4e2bea

  Copy full SHA for d4e2bea

Commits on Mar 26, 2020

• adding back experiment with propositional resolution

  

  Thibault Gauthier

  committed
  f1fba3b

  Copy full SHA for f1fba3b

Commits on Mar 25, 2020

• save before battery crash

  

  Thibault Gauthier

  committed
  15067f2

  Copy full SHA for 15067f2

• Fix proofs broken by 508f79e

  

  Michael Norrish

  committed
  6b4719d

  Copy full SHA for 6b4719d

Commits on Mar 24, 2020

• Fix unification/triangular/first-order given previous commit

  Show description for 59c10c6
  

  Michael Norrish

  committed
  59c10c6

  Copy full SHA for 59c10c6

• Use new syntax more in unification/triangular/nominal

  

  Michael Norrish

  committed
  9d069ef

  Copy full SHA for 9d069ef

• Fix proof broken by 508f79e

  

  Michael Norrish

  committed
  4f9d5fe

  Copy full SHA for 4f9d5fe

• emacs-mode: fix bug in goal-finding (M-h g) with Triviality keyword

  Show description for a51789c
  

  Michael Norrish

  committed
  a51789c

  Copy full SHA for a51789c

Pagination

Previous

Next