Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Jan 30, 2026

• Added a proof of Urysohn's metrization theorem and also a definition of set

  Show description for c845dd3
  jrh13

  committed
  c845dd3

  Copy full SHA for c845dd3

Commits on Jan 9, 2026

• Merge pull request #149 from aqjune-aws/fix-tactictrace

  Show description for e960dd0
  jrh13

  authored
  e960dd0

  Copy full SHA for e960dd0

Commits on Dec 11, 2025

• Remove holtest, add NUMCORES to holtest_parallel

  aqjune-aws

  committed
  18c7e08

  Copy full SHA for 18c7e08

• Fix TacticTrace to support OCaml 5.4, add 'hol.sh compile/link/inline-load/-use-module'

  Show description for b8ca210
  aqjune-aws

  committed
  b8ca210

  Copy full SHA for b8ca210

• Made a small fix in WORD_SIMPLE_SUBWORD_CONV, which was failing to

  Show description for b9a430b
  jrh13

  committed
  b9a430b

  Copy full SHA for b9a430b

Commits on Nov 18, 2025

• Merge pull request #148 from aqjune-aws/ocaml5.4.0

  Show description for 08bcac7
  jrh13

  authored
  08bcac7

  Copy full SHA for 08bcac7

Commits on Nov 17, 2025

• Add update_database_5.4.ml, add chooser.sh for database, update github CI to test its loading

  aqjune-aws

  committed
  0909bea

  Copy full SHA for 0909bea

• Support OCaml 5.4 and latest camlp5, minor improvements

  Show description for 4adc282
  aqjune-aws

  committed
  4adc282

  Copy full SHA for 4adc282

Commits on Oct 23, 2025

• Added a couple more theorems about subwords of composite terms:

  Show description for c41aea3
  jrh13

  committed
  c41aea3

  Copy full SHA for c41aea3

Commits on Sep 22, 2025

• Merge pull request #145 from aqjune-aws/taclog

  Show description for bed58fa
  jrh13

  authored
  bed58fa

  Copy full SHA for bed58fa

• Merge pull request #144 from Deducteam/sqrt

  Show description for 2f1cae4
  jrh13

  authored
  2f1cae4

  Copy full SHA for 2f1cae4

Commits on Sep 2, 2025

• Add TacticTrace for logging input/outputs of tactics and conversions

  aqjune-aws

  committed
  9b56951

  Copy full SHA for 9b56951

Commits on Aug 30, 2025

• use float_sqrt instead

  fblanqui

  committed
  44c6400

  Copy full SHA for 44c6400

Commits on Aug 5, 2025

• metis.ml: qualify sqrt by Stdlib (one occurrence) to avoid a typing error in some cases

  fblanqui

  committed
  f74212a

  Copy full SHA for f74212a

Commits on Jul 16, 2025

• Merge pull request #142 from aqjune-aws/camlp5_8.03.06

  Show description for 157c99b
  jrh13

  authored
  157c99b

  Copy full SHA for 157c99b

Commits on Jul 15, 2025

• github ci: add opam archive

  aqjune-aws

  committed
  76e8cc9

  Copy full SHA for 76e8cc9

• Add support for camlp5 8.03.06

  Show description for 0c718bd
  aqjune-aws

  committed
  0c718bd

  Copy full SHA for 0c718bd

Commits on Jul 4, 2025

• Adopted a patch from Dan Bernstein to replace the use of pointer-level

  Show description for 647a92b
  jrh13

  committed
  647a92b

  Copy full SHA for 647a92b

Commits on Jun 19, 2025

• Merge pull request #141 from aqjune-aws/ver310

  Show description for 37af947
  jrh13

  authored
  37af947

  Copy full SHA for 37af947

• Add dependent packages to the CI check of OCaml 4.06, fix error detection

  aqjune-aws

  committed
  6794be8

  Copy full SHA for 6794be8

Commits on Jun 17, 2025

• Added material about algebraic dependence and transcendence bases to

  Show description for 3b5c9db
  jrh13

  committed
  3b5c9db

  Copy full SHA for 3b5c9db

Commits on Jun 12, 2025

• Increment the version, backport the update of opam file

  Show description for 50833f5
  aqjune-aws

  committed
  50833f5

  Copy full SHA for 50833f5

Commits on Jun 7, 2025

• Merge pull request #140 from aqjune-aws/tactic_er

  Show description for 0b58b1a
  jrh13

  authored
  0b58b1a

  Copy full SHA for 0b58b1a

Commits on Jun 6, 2025

• Add a new command 'er' to the subgoal package

  Show description for 3e25a30
  aqjune-aws

  committed
  3e25a30

  Copy full SHA for 3e25a30

Commits on May 30, 2025

• Merge pull request #138 from aqjune-aws/benign_redef_ind

  Show description for 8ee43fa
  jrh13

  authored
  8ee43fa

  Copy full SHA for 8ee43fa

Commits on May 29, 2025

• Allow benign redefinition in new_inductive_definition when extra foralls are added

  Show description for 0143dee
  aqjune-aws

  committed
  0143dee

  Copy full SHA for 0143dee

Commits on May 24, 2025

• Added some theory about field extensions: properties of algebraic,

  Show description for cddb65d
  jrh13

  committed
  cddb65d

  Copy full SHA for cddb65d

Commits on May 21, 2025

• Made some more additions to matroid and ring background theory, in

  Show description for cf4d1f3
  jrh13

  committed
  cf4d1f3

  Copy full SHA for cf4d1f3

• Merge pull request #137 from jargh/master

  Show description for a570c68
  jrh13

  authored
  a570c68

  Copy full SHA for a570c68

• Merge branch 'jrh13:master' into master

  jargh

  authored
  289240e

  Copy full SHA for 289240e

• Merge pull request #133 from aqjune-aws/colprint

  Show description for 025a7ce
  jrh13

  authored
  025a7ce

  Copy full SHA for 025a7ce

Commits on May 20, 2025

• Merge pull request #136 from jargh/master

  Show description for 2ee50ee
  jrh13

  authored
  2ee50ee

  Copy full SHA for 2ee50ee

• Add more list lemmas and list function evaluation conversions

  Show description for c0953a8
  jargh

  committed
  c0953a8

  Copy full SHA for c0953a8

• Merge branch 'jrh13:master' into master

  jargh

  authored
  aaeee7f

  Copy full SHA for aaeee7f

Commits on May 2, 2025

• Merge branch 'master' into colprint

  aqjune-aws

  committed
  63178ed

  Copy full SHA for 63178ed

Pagination

Previous

Next