Isabelle-HoTT/ROOT, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 Bad practice huge commit: 2021-06-24T21:40:05+00:00 Josh Chen 2021-06-24T21:40:05+00:00 f988d541364841cd208f4fd21ff8e5e2935fc7aa 1. Rudimentary prototype definitional package 2. Started univalence 3. Various compatibility fixes and new theory stubs 4. Updated ROOT file 
1. Rudimentary prototype definitional package
2. Started univalence
3. Various compatibility fixes and new theory stubs
4. Updated ROOT file
rename things + some small changes 2021-01-31T02:54:51+00:00 Josh Chen 2021-01-31T02:54:51+00:00 2feb56660700af107abb5a28a7120052ac405518 






Forgot to update ROOT
2021-01-19T02:44:03+00:00

Josh Chen

2021-01-19T02:44:03+00:00

6d8fa47f205e24a94416279fab41f09db6f02b8b












(FEAT) Term elaboration of assumption and goal statements.
2020-07-31T12:56:24+00:00

Josh Chen

2020-07-31T12:56:24+00:00

ff5454812f9e2720bd90c3a5437505644f63b487

  . spartan/core/goals.ML
  . spartan/core/elaboration.ML
  . spartan/core/elaborated_statement.ML

(FEAT) More context tacticals and search tacticals.
  . spartan/core/context_tactical.ML

(FEAT) Improved subgoal focus.
  Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
  . spartan/core/focus.ML

(FIX) Normalize facts in order to be able to resolve properly.
  . spartan/core/typechecking.ML

(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.





  . spartan/core/goals.ML
  . spartan/core/elaboration.ML
  . spartan/core/elaborated_statement.ML

(FEAT) More context tacticals and search tacticals.
  . spartan/core/context_tactical.ML

(FEAT) Improved subgoal focus.
  Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
  . spartan/core/focus.ML

(FIX) Normalize facts in order to be able to resolve properly.
  . spartan/core/typechecking.ML

(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.







reorganize
2020-06-19T10:41:54+00:00

Josh Chen

2020-06-19T10:41:54+00:00

4f147cba894baa9e372e2b67211140b1a6f7b16c












fix ROOT
2020-06-15T09:58:30+00:00

Josh Chen

2020-06-15T09:58:30+00:00

8885f9c96d950655250292ee03b54aafeb2f727f












clean up Eckmann-Hilton and move to Identity
2020-05-29T08:37:46+00:00

Josh Chen

2020-05-29T08:37:46+00:00

2f4e9b941a01a789b17fe208687a27060990e0a7












reorganize folder structure
2020-05-28T10:54:40+00:00

Josh Chen

2020-05-28T10:54:40+00:00

a9606c980dcc32ade28ebd1515cad33b380ebd64












move More_Types to Spartan
2020-05-27T19:30:21+00:00

Josh Chen

2020-05-27T19:30:21+00:00

ec7dcd5e780d26e7f8866c3d245b08b23de56ff9












Eckmann-Hilton, first pass
2020-05-26T23:18:46+00:00

Josh Chen

2020-05-26T23:18:46+00:00

fd8ae0b89a703443ef625ca243e6d5ecfa7b2271