Commits

Breadcrumbs

History for

ondevelop

User selector

All users

Datepicker

All time

Commit History

Commits on Jul 10, 2020

• Extend drule family with rev_ and _at options

  Show description for e74b9be
  

  Michael Norrish

  committed
  e74b9be

• Prove that pushouts in Set are unique up to isomorphism

  Show description for f529d31
  

  Michael Norrish

  committed
  f529d31

• Improve simp to automatically handle numerals as arguments to case

  Show description for 415aca0
  

  Michael Norrish

  committed
  415aca0

Commits on Jul 8, 2020

• Fix another use of PAT_ASSUM that quotes existing variables

  

  Michael Norrish

  committed
  6f28c73

• Tidy up output of selftest in num/termination

  

  Michael Norrish

  committed
  f6af3fe

• Fix bug in PAT_ASSUM when use of variables from goal is not respected

  Show description for b60b7b7
  

  Michael Norrish

  committed
  b60b7b7

• Improve propagation of error messages out of goal_assum

  

  Michael Norrish

  committed
  b1ae06f

• Fix a resolve_then bug when the goal should be completely solved

  

  Michael Norrish

  committed
  baab4a8

Commits on Jul 6, 2020

• Fix Unicode violation in 12f41f3

  

  Michael Norrish

  committed
  6f97b57

• Remove dependency of ord*Notation theories on basis_emit

  Show description for 31cafa9
  

  Michael Norrish

  committed
  31cafa9

Commits on Jul 3, 2020

• Fix typos and separate equivalence thms

  

  myreen

  authored and

  Michael Norrish

  committed
  79ddaf4

• Add a theory about lazy (rose) trees to src/coalgebras

  

  myreen

  authored and

  Michael Norrish

  committed
  12f41f3

Commits on Jul 1, 2020

• Add a little lemma about pushouts in Set

  

  Michael Norrish

  committed
  2fbeb04

• Clean up optionScript in a variety of ways

  Show description for 29d12c4
  

  Michael Norrish

  committed
  29d12c4

• Fix bug in Induct_on somerel when args included var x and non-var

  Show description for 94368c1
  

  Michael Norrish

  committed
  94368c1

Commits on Jun 29, 2020

• Fix selftest broken by 5c27284 (it wanted to use flip as a var)

  

  Michael Norrish

  committed
  3f7c783

• Promote mp_then and resolve_then to be exported by Tactic

  Show description for 1f5a1e1
  

  Michael Norrish

  committed
  1f5a1e1

• Make FullUnify only depend on boolSyntax, not boolLib

  

  Michael Norrish

  committed
  1cec313

• Move some term-equality helper functions from boolLib to boolSyntax

  Show description for 0a473a3
  

  Michael Norrish

  committed
  0a473a3

• Add flip as an alias for combin$C

  

  Michael Norrish

  committed
  5c27284

Commits on Jun 28, 2020

• Fix Unicode violations

  

  Michael Norrish

  committed
  ee7dc5d

Commits on Jun 26, 2020

• Prove some basic category theory results (over Set) in coalgAxioms

  Show description for 88ac6ec
  

  Michael Norrish

  committed
  88ac6ec

• Define a disjoint-union function ('a set -> 'b set -> ('a + 'b) set)

  

  Michael Norrish

  committed
  31b3ff6

• Prove a "deep intro" rule for pred_set$CHOICE (for DEEP_INTRO_TAC)

  Show description for a0625e3
  

  Michael Norrish

  committed
  a0625e3

Commits on Jun 23, 2020

• Prove a chunk of Rutten's Theorem 7.1 (First Isomorphism theorem)

  

  Michael Norrish

  committed
  0aae644

• More co-algebra mechanisation, mostly done with Rutten §6

  

  Michael Norrish

  committed
  f9f2989

Commits on Jun 22, 2020

• Remove some Unicode in src

  

  Michael Norrish

  committed
  de873d0

• align numeric syntax: 'great' becomes 'greater' The earlier names are inconsistent with numSyntax and less descriptive.

  Show description for d2b57f0
  

  arolle

  authored and

  Michael Norrish

  committed
  d2b57f0

• remove lcsymtacs (github issue HOL-Theorem-Prover#666)

  Show description for 5417af9
  

  arolle

  authored and

  Michael Norrish

  committed
  5417af9

Commits on Jun 21, 2020

• Fix monadic while in error-state monad

  

  hrutvik

  authored and

  Michael Norrish

  committed
  336bf73

Commits on Jun 20, 2020

• Fix Unicode violation in src/

  

  Michael Norrish

  committed
  3ff35df

Commits on Jun 19, 2020

• For some reason I cannot build acmart-based articles when makeidx is loaded

  

  AndreasLoow

  authored and

  Michael Norrish

  committed
  df9c20a

Commits on Jun 18, 2020

• More progress on mechanising Rutten

  

  Michael Norrish

  committed
  a3801dd

Commits on Jun 17, 2020

• Make some Unicode parenthesis-like characters non-aggregating

  Show description for 8eabfe9
  

  Michael Norrish

  committed
  8eabfe9

• Start of some abstract mechanisation of coalgebra theory

  

  Michael Norrish

  committed
  0f36377

Pagination

PreviousNext