Isabelle-HoTT/spartan/data, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 remove old folder 2020-06-15T09:56:28+00:00 Josh Chen 2020-06-15T09:56:28+00:00 28e91f960d7b41f3658a2736f7d87ba5e79f87f6 






1. Type information context data
2020-06-03T11:09:30+00:00

Josh Chen

2020-06-03T11:09:30+00:00

e513fc2958133e3a00c06ebcd1214741843acf08

2. Small reformulations of rules
3. Bool





2. Small reformulations of rules
3. Bool







reorganize and add some material
2020-06-01T15:19:27+00:00

Josh Chen

2020-06-01T15:19:27+00:00

29112d66eb3ecf4139db1da16878d8a817640696












more list
2020-05-31T11:14:35+00:00

Josh Chen

2020-05-31T11:14:35+00:00

dc3800fa4e98e8feeae86f95bf4aafb80f01880c












bit more material
2020-05-28T14:00:42+00:00

Josh Chen

2020-05-28T14:00:42+00:00

417af1adf5453720c55e27de212b830569311f0e












more List and Maybe
2020-05-28T12:08:26+00:00

Josh Chen

2020-05-28T12:08:26+00:00

1ccd93665a01acdc25b37409e94b71615ced5393












change variable name in elim rules and fix small mistake
2020-05-27T20:16:42+00:00

Josh Chen

2020-05-27T20:16:42+00:00

f12983b1b53c71fc416155ac4b7e2b11ed8ca9ef












1. Define Maybe in terms of other types. 2. Move More_Types to Spartan
2020-05-27T19:31:35+00:00

Josh Chen

2020-05-27T19:31:35+00:00

62c1c8f306bff84b74b3b1c935d0d6722e1251a2












Maybe and more List
2020-05-26T14:39:35+00:00

Josh Chen

2020-05-26T14:39:35+00:00

8ba8357a0b4640a3be817fd0645d026b568bc552












notation
2020-05-25T17:36:30+00:00

Josh Chen

2020-05-25T17:36:30+00:00

c19533acfad3bbe603cd8a3d176e8b14f477573a