| #
5417af9d |
|
31-Mar-2020 |
Arve Gengelbach <arve.gengelbach@it.uu.se> |
remove lcsymtacs (github issue #666)
The lcsymtacs structure is regarded superseded as it plainly is
a shorthand for opening the following modules:
Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib
Rewrite bossLib Thm_cont
|
| #
0882334d |
|
12-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix examples/set-theory/zfset for tight equality
|
| #
bd77b8fb |
|
20-Oct-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Delete trailing whitespace
|
| #
c775cd0c |
|
26-Mar-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Start on an axiomatization of VBG set theory.
Create new container directory set-theory in examples to hold this and
the existing zfc stuff.
|