src/HOL/Import/HOL/combin.imp
changeset 14516 a183dec876ab
child 44763 b50d5d694838
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL/combin.imp	Fri Apr 02 17:37:45 2004 +0200
@@ -0,0 +1,41 @@
+import
+
+import_segment "hol4"
+
+def_maps
+  "W" > "W_def"
+  "S" > "S_def"
+  "K" > "K_def"
+  "I" > "I_def"
+  "C" > "C_def"
+
+const_maps
+  "o" > "Fun.comp"
+  "W" > "HOL4Base.combin.W"
+  "S" > "HOL4Base.combin.S"
+  "K" > "HOL4Base.combin.K"
+  "I" > "HOL4Base.combin.I"
+  "C" > "HOL4Base.combin.C"
+
+thm_maps
+  "o_THM" > "Fun.o_apply"
+  "o_DEF" > "Fun.o_apply"
+  "o_ASSOC" > "Fun.o_assoc"
+  "W_def" > "HOL4Base.combin.W_def"
+  "W_THM" > "HOL4Base.combin.W_def"
+  "W_DEF" > "HOL4Base.combin.W_DEF"
+  "S_def" > "HOL4Base.combin.S_def"
+  "S_THM" > "HOL4Base.combin.S_def"
+  "S_DEF" > "HOL4Base.combin.S_DEF"
+  "K_def" > "HOL4Base.combin.K_def"
+  "K_THM" > "HOL4Base.combin.K_def"
+  "K_DEF" > "HOL4Base.combin.K_DEF"
+  "I_o_ID" > "HOL4Base.combin.I_o_ID"
+  "I_def" > "HOL4Base.combin.I_def"
+  "I_THM" > "HOL4Base.combin.I_THM"
+  "I_DEF" > "HOL4Base.combin.I_DEF"
+  "C_def" > "HOL4Base.combin.C_def"
+  "C_THM" > "HOL4Base.combin.C_def"
+  "C_DEF" > "HOL4Base.combin.C_DEF"
+
+end