Commits

Branch selector

 develop

User selector

All users

Datepicker

All time

Commit History

Commits on Jul 11, 2024

• Merge branch 'HOL-Theorem-Prover:develop' into develop

  xdrr

  authored
  c127ea2

Commits on Jul 2, 2024

• Get help/src-sml to build again after 7c55b699b9714

  mn200

  committed
  a004768

• Fix bug in normalisation of multiplicative terms over ℝ

  Show description for 582373f
  mn200

  committed
  582373f

• Slightly reorganise library code manipulating quotations

  Show description for 1023627
  mn200

  committed
  1023627

• DES properties added (HOL-Theorem-Prover#1264)

  Show description for 1bdff85
  gengarrrr

  authored
  1bdff85

• FTBFS boehmTheory (due to code merging issue)

  

  binghe

  authored and

  mn200

  committed
  fd9093e

• Stage work on the lambda example (BT_subterm_thm, etc.)

  

  binghe

  authored and

  mn200

  committed
  36e026a

Commits on Jun 29, 2024

• Remove more THENLs

  

  IlmariReissumies

  authored and

  mn200

  committed
  9650cff

• Explain >- where it's first used in euclid

  

  IlmariReissumies

  authored and

  mn200

  committed
  f8fe4e4

• Fix a proof

  

  IlmariReissumies

  authored and

  mn200

  committed
  eace0ce

• Extirpate >| from combinator section

  

  IlmariReissumies

  authored and

  mn200

  committed
  6607d82

• Extirpate >| from euclid tute

  

  IlmariReissumies

  authored and

  mn200

  committed
  ca81aa8

• Replace THENL with THEN1 in HOL logic chapter

  

  IlmariReissumies

  authored and

  mn200

  committed
  55addba

Commits on Jun 28, 2024

• Add NOT_AND' (|- ~(~t /\ t)) to BOOL_ss (in addition to NOT_AND: |- ~(t /\ ~t))

  

  binghe

  authored and

  mn200

  committed
  8939159

• Fix a failure to generate sufficient fresh names in one_line_ify

  Show description for ee366f3
  mn200

  committed
  ee366f3

• Adds mrec and interp combinators

  xdrr

  committed
  d0bea38

Commits on Jun 18, 2024

• Remove some unicode

  

  myreen

  authored and

  mn200

  committed
  493fc3f

• Add COUNT_LIST cv_inline theorem

  Show description for 8ec5529
  

  2 peopleauthored and

  mn200

  committed
  8ec5529

• Fix bug introduced in last commit

  

  hrutvik

  authored and

  mn200

  committed
  769d833

• Add int_{mod,div} cv_rep theorems

  Show description for b3a19d3
  

  2 peopleauthored and

  mn200

  committed
  b3a19d3

• Add cv_rep theorems for natural >, >=

  

  hrutvik

  authored and

  mn200

  committed
  2353032

• Sketch a new selftest

  

  myreen

  authored and

  mn200

  committed
  92a4e57

• Improve cv_eval error message

  

  myreen

  authored and

  mn200

  committed
  3d55e6b

Commits on Jun 17, 2024

• Move NUM_FLOOR/NUM_CEILING to realaxTheory (HOL-Theorem-Prover#1256)

  Show description for 04f56f8
  binghe

  authored
  04f56f8

• [release-notes] document change to numLib.prefer_num

  mn200

  committed
  212343b

• [release-notes] tweak wording about new src/algebra theories

  mn200

  committed
  299786b

Commits on Jun 16, 2024

• Remove some uses of >> for THEN1

  mn200

  committed
  12a868b

• Remove some long commented-out code

  mn200

  committed
  d1719a6

• Rename prefer_num to temp_...; use old name for permanent change

  Show description for 0a75ce8
  mn200

  committed
  0a75ce8

Commits on Jun 15, 2024

• Fixed C++ compilation failure of zc2hs on macOS

  

  binghe

  authored and

  mn200

  committed
  3972bf8

Commits on Jun 12, 2024

• Minor updates to powr_def (more friendly as rewriting rules)

  

  binghe

  authored and

  mn200

  committed
  e087c0b

• FTBFS due to changes of rpow_def

  

  binghe

  authored and

  mn200

  committed
  5e029c1

• Extended domain of rpow (powr)

  

  binghe

  authored and

  mn200

  committed
  08aa342

• Avoid calling tailrec_define on non-recursive definitions

  

  Magnus Myreen

  authored and

  mn200

  committed
  ce28fb9

• Add dest_path to Conv

  

  Magnus Myreen

  authored and

  mn200

  committed
  b67a714

Pagination

Previous

Next