Commits

Branch selector

 develop

User selector

All users

Datepicker

All time

Commit History

Commits on Mar 19, 2024

• Handle natural number subtraction under & better in int d.p.'s

  Show description for 1a1b46d
  mn200

  committed
  1a1b46d

  Copy full SHA for 1a1b46d

• Fix handling of Num in line with its new semantics

  Show description for 5788053
  mn200

  committed
  5788053

  Copy full SHA for 5788053

Commits on Mar 18, 2024

• Updated HOL Description with higher mathematics contents promoted to chapter level

  

  binghe

  authored and

  mn200

  committed
  671b4b7

  Copy full SHA for 671b4b7

• Add clearer error on double implication in inductive definitions

  Show description for 9ac238f
  

  mrichards30

  authored and

  mn200

  committed
  9ac238f

  Copy full SHA for 9ac238f

Commits on Mar 15, 2024

• Document DB.selectDB; tweak doc file for DB.find

  mn200

  committed
  9f96ab9

  Copy full SHA for 9f96ab9

• Clean up some doc-files; preferring not to use alpha --> bool syntax

  Show description for cf3fab2
  mn200

  committed
  cf3fab2

  Copy full SHA for cf3fab2

• Fix bug in holfoot that let its parser get contaminated by others'

  Show description for 01d5d9a
  mn200

  committed
  01d5d9a

  Copy full SHA for 01d5d9a

Commits on Mar 14, 2024

• Fix bug in Omega test

  Show description for e8b3178
  mn200

  committed
  e8b3178

  Copy full SHA for e8b3178

• Upgrade integer DP testing code to use testutils

  mn200

  committed
  b9bd54b

  Copy full SHA for b9bd54b

• Fix a bug in PIntMap.size

  mn200

  committed
  eeb10e8

  Copy full SHA for eeb10e8

Commits on Mar 12, 2024

• Better statements of Boehm_transform_exists_lemma

  

  binghe

  authored and

  mn200

  committed
  29e263e

  Copy full SHA for 29e263e

• [lambda] Boehm_transform_exists_lemma (Lemma 10.3.6 (ii) [1, p.247])

  

  binghe

  authored and

  mn200

  committed
  5314eb3

  Copy full SHA for 5314eb3

• HolSmt: fix Z3 proof replay of asserted proof rules

  Show description for fbaa3a9
  

  someplaceguy

  authored and

  mn200

  committed
  fbaa3a9

  Copy full SHA for fbaa3a9

• HolSmt: add four rewrite theorems for Z3 proof replay

  Show description for c725a1a
  

  someplaceguy

  authored and

  mn200

  committed
  c725a1a

  Copy full SHA for c725a1a

• HolSmt: replay sk inference rule in Z3 proofs

  Show description for 823e649
  

  someplaceguy

  authored and

  mn200

  committed
  823e649

  Copy full SHA for 823e649

• HolSmt: fix elim-unused proof rule to work w/ exists quantifiers

  Show description for f3f5e21
  

  someplaceguy

  authored and

  mn200

  committed
  f3f5e21

  Copy full SHA for f3f5e21

• HolSmt: fix quant-intro proof rule to work w/ exists quantifiers

  Show description for c488a6c
  

  someplaceguy

  authored and

  mn200

  committed
  c488a6c

  Copy full SHA for c488a6c

• HolSmt: build an smtheap

  Show description for 466d6c2
  

  someplaceguy

  authored and

  mn200

  committed
  466d6c2

  Copy full SHA for 466d6c2

• HolSmt: enable Z3 proof replay of num self-tests

  Show description for 68f30d6
  

  someplaceguy

  authored and

  mn200

  committed
  68f30d6

  Copy full SHA for 68f30d6

• HolSmt: work around Z3 quant-inst proof rule issue

  Show description for 9f055e4
  

  someplaceguy

  authored and

  mn200

  committed
  9f055e4

  Copy full SHA for 9f055e4

• HolSmt: work around ARITH_PROVE bug

  Show description for 194563d
  

  someplaceguy

  authored and

  mn200

  committed
  194563d

  Copy full SHA for 194563d

• HolSmt: parse proof-bind rules in Z3 proofs

  Show description for 7724583
  

  someplaceguy

  authored and

  mn200

  committed
  7724583

  Copy full SHA for 7724583

• HolSmt: replay refl inference rule in Z3 proofs

  Show description for 355248c
  

  someplaceguy

  authored and

  mn200

  committed
  355248c

  Copy full SHA for 355248c

• HolSmt: parse lambda binders in Z3 proofs

  Show description for 1c6e508
  

  someplaceguy

  authored and

  mn200

  committed
  1c6e508

  Copy full SHA for 1c6e508

• HolSmt: parse nested let bindings in Z3 proofs

  Show description for 193cfe1
  

  someplaceguy

  authored and

  mn200

  committed
  193cfe1

  Copy full SHA for 193cfe1

• HolSmt: parametrize the SMT-LIB parser by let handling functions

  Show description for 16e6d94
  

  someplaceguy

  authored and

  mn200

  committed
  16e6d94

  Copy full SHA for 16e6d94

• HolSmt: rename nums -> indices

  Show description for 0fb203f
  

  someplaceguy

  authored and

  mn200

  committed
  0fb203f

  Copy full SHA for 0fb203f

• HolSmt: replay quant-inst rule in Z3 v4 proofs

  Show description for 9640aee
  

  someplaceguy

  authored and

  mn200

  committed
  9640aee

  Copy full SHA for 9640aee

• HolSmt: parse indexed identifiers' indices as terms

  Show description for f51b787
  

  someplaceguy

  authored and

  mn200

  committed
  f51b787

  Copy full SHA for f51b787

• HolSmt: replay mp~ proof rule in Z3 v4 proofs

  Show description for 043537b
  

  someplaceguy

  authored and

  mn200

  committed
  043537b

  Copy full SHA for 043537b

• HolSmt: print invalid proofterms

  Show description for 8932bbb
  

  someplaceguy

  authored and

  mn200

  committed
  8932bbb

  Copy full SHA for 8932bbb

• HolSmt: replay the nnf-neg and nnf-pos proof rules

  Show description for c49e07b
  

  someplaceguy

  authored and

  mn200

  committed
  c49e07b

  Copy full SHA for c49e07b

• HolSmt: make sure let definitions use unique names in Z3 proofs

  Show description for 7aea54b
  

  someplaceguy

  authored and

  mn200

  committed
  7aea54b

  Copy full SHA for 7aea54b

• HolSmt: hoist Z3 proof let parsing into separate function

  Show description for cc836c9
  

  someplaceguy

  authored and

  mn200

  committed
  cc836c9

  Copy full SHA for cc836c9

• HolSmt: disable Z3 v2 on failing test cases

  Show description for 72c0ab0
  

  someplaceguy

  authored and

  mn200

  committed
  72c0ab0

  Copy full SHA for 72c0ab0

Pagination

Previous

Next