From bf4894f81dfecc1f45016312c4e703f40fbdbc0a Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 6 Aug 2020 13:26:25 +0200 Subject: [PATCH] Get another file to build again --- candle/set-theory/setModelScript.sml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/candle/set-theory/setModelScript.sml b/candle/set-theory/setModelScript.sml index 0fda8d743e..cf24aa673d 100644 --- a/candle/set-theory/setModelScript.sml +++ b/candle/set-theory/setModelScript.sml @@ -6,6 +6,10 @@ open preamble bitTheory setSpecTheory val _ = new_theory"setModel" +val _ = temp_delsimps ["NORMEQ_CONV"] +val _ = diminish_srw_ss ["ABBREV"] +val _ = set_trace "BasicProvers.var_eq_old" 1 + val is_set_theory_pred_def = Define` is_set_theory_pred is_v_rep in_rep ⇔ (∃x. is_v_rep x) ∧