src/HOL/Import/HOL/bword_arith.imp
changeset 14516 a183dec876ab
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL/bword_arith.imp	Fri Apr 02 17:37:45 2004 +0200
@@ -0,0 +1,27 @@
+import
+
+import_segment "hol4"
+
+def_maps
+  "ICARRY" > "ICARRY_def"
+  "ACARRY" > "ACARRY_def"
+
+thm_maps
+  "WSEG_NBWORD_ADD" > "HOL4Vec.bword_arith.WSEG_NBWORD_ADD"
+  "ICARRY_WSEG" > "HOL4Vec.bword_arith.ICARRY_WSEG"
+  "ICARRY_DEF" > "HOL4Vec.bword_arith.ICARRY_DEF"
+  "BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.BNVAL_LESS_EQ"
+  "ADD_WORD_SPLIT" > "HOL4Vec.bword_arith.ADD_WORD_SPLIT"
+  "ADD_NBWORD_EQ0_SPLIT" > "HOL4Vec.bword_arith.ADD_NBWORD_EQ0_SPLIT"
+  "ADD_BV_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ1"
+  "ADD_BV_BNVAL_LESS_EQ" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_LESS_EQ"
+  "ADD_BV_BNVAL_DIV_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BV_BNVAL_DIV_LESS_EQ1"
+  "ADD_BNVAL_LESS_EQ1" > "HOL4Vec.bword_arith.ADD_BNVAL_LESS_EQ1"
+  "ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_WSEG"
+  "ACARRY_MSB" > "HOL4Vec.bword_arith.ACARRY_MSB"
+  "ACARRY_EQ_ICARRY" > "HOL4Vec.bword_arith.ACARRY_EQ_ICARRY"
+  "ACARRY_EQ_ADD_DIV" > "HOL4Vec.bword_arith.ACARRY_EQ_ADD_DIV"
+  "ACARRY_DEF" > "HOL4Vec.bword_arith.ACARRY_DEF"
+  "ACARRY_ACARRY_WSEG" > "HOL4Vec.bword_arith.ACARRY_ACARRY_WSEG"
+
+end