Skip to content
Permalink
Browse files

Adjust a few files for tightequality

  • Loading branch information...
myreen committed Jun 29, 2019
1 parent 71e11ac commit 87babfca481c23ef70165c34d3fc7802ff5d10a0
@@ -6,6 +6,7 @@ open HolKernel Parse boolLib bossLib; val _ = new_theory "copying_gc";
open pred_setTheory arithmeticTheory pairTheory listTheory combinTheory;
open finite_mapTheory sumTheory relationTheory;

val _ = ParseExtras.temp_loose_equality();

val _ = Hol_datatype `heap_address = H_ADDR of num | H_DATA of 'a`;

@@ -6,6 +6,8 @@ open TotalDefn numLib prim_recTheory arithmeticTheory;

val _ = new_theory "ninetyOne"

val _ = ParseExtras.temp_loose_equality()

(*---------------------------------------------------------------------------
Define the 91 function. We call it "N". We use Hol_defn to
make the definition, since we have to tackle the termination
@@ -38,6 +38,7 @@ open HolKernel bossLib Theory Parse Tactic boolLib Lib
open stringLib pairTheory arithmeticTheory listTheory optionTheory;

val thm_counter = Count.mk_meter();
val _ = ParseExtras.temp_loose_equality();

(*---------------------------------------------------------------------------*)
(* Change free variable names to desired ones. Takes a list of (old,new) *)

0 comments on commit 87babfc

Please sign in to comment.
You can’t perform that action at this time.