From 188566719d28a140602a24ef823b28b81e45cb85 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 16 Apr 2020 15:37:43 +0200 Subject: update for Isabelle2020 --- README.md | 6 +++--- ROOT | 1 + spartan/lib/equality.ML | 2 +- spartan/lib/goals.ML | 2 +- 4 files changed, 6 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 879b5d3..a5b7ef5 100644 --- a/README.md +++ b/README.md @@ -4,11 +4,11 @@ An experimental implementation of [homotopy type theory](https://en.wikipedia.or ### Usage -Isabelle/HoTT is compatible with Isabelle2019. -To use, add the Isabelle/HoTT folder path to `.isabelle/Isabelle2019/ROOTS` (on Mac/Linux/cygwin installations): +Isabelle/HoTT is compatible with Isabelle2020. +To use, add the Isabelle/HoTT folder path to `.isabelle/Isabelle2020/ROOTS` (on Mac/Linux/cygwin installations): ``` -echo >> ~/.isabelle/Isabelle2019/ROOTS +echo >> ~/.isabelle/Isabelle2020/ROOTS ``` ### What (and why) is this? diff --git a/ROOT b/ROOT index 218dc9c..09e3042 100644 --- a/ROOT +++ b/ROOT @@ -22,3 +22,4 @@ session HoTT in hott = Spartan + theories Base Nat + diff --git a/spartan/lib/equality.ML b/spartan/lib/equality.ML index 79b4086..023147b 100644 --- a/spartan/lib/equality.ML +++ b/spartan/lib/equality.ML @@ -84,7 +84,7 @@ fun equality_context_tac fact ctxt = THEN ALLGOALS (side_conds_tac ctxt) ) in - fn (ctxt, st) => Method.CONTEXT (record_inserts ctxt) (tac st) + fn (ctxt, st) => Context_Tactic.TACTIC_CONTEXT (record_inserts ctxt) (tac st) end end diff --git a/spartan/lib/goals.ML b/spartan/lib/goals.ML index ce23751..9f394f0 100644 --- a/spartan/lib/goals.ML +++ b/spartan/lib/goals.ML @@ -31,7 +31,7 @@ fun prep_statement prep_att prep_stmt raw_elems raw_stmt ctxt = let val (stmt, elems_ctxt) = prep_stmt raw_elems raw_stmt ctxt val prems = Assumption.local_prems_of elems_ctxt ctxt - val stmt_ctxt = fold (fold (Variable.auto_fixes o fst) o snd) + val stmt_ctxt = fold (fold (Proof_Context.augment o fst) o snd) stmt elems_ctxt in case raw_stmt of -- cgit v1.2.3