src/HOL/Import/HOL4/Generated/boolean_sequence.imp
changeset 47259 2d4ea84278da
parent 47258 880e587eee9f
child 47260 3b9eeb4a2967
--- a/src/HOL/Import/HOL4/Generated/boolean_sequence.imp	Sun Apr 01 14:50:47 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-import
-
-import_segment "hol4"
-
-def_maps
-  "STL" > "STL_primdef"
-  "STAKE" > "STAKE_primdef"
-  "SHD" > "SHD_primdef"
-  "SDROP" > "SDROP_primdef"
-  "SDEST" > "SDEST_primdef"
-  "SCONST" > "SCONST_primdef"
-  "SCONS" > "SCONS_primdef"
-
-const_maps
-  "STL" > "HOL4Prob.boolean_sequence.STL"
-  "SHD" > "HOL4Prob.boolean_sequence.SHD"
-  "SDEST" > "HOL4Prob.boolean_sequence.SDEST"
-  "SCONST" > "HOL4Prob.boolean_sequence.SCONST"
-
-thm_maps
-  "STL_primdef" > "HOL4Prob.boolean_sequence.STL_primdef"
-  "STL_def" > "HOL4Prob.boolean_sequence.STL_def"
-  "STL_SCONST" > "HOL4Prob.boolean_sequence.STL_SCONST"
-  "STL_SCONS" > "HOL4Prob.boolean_sequence.STL_SCONS"
-  "STAKE_def" > "HOL4Prob.boolean_sequence.STAKE_def"
-  "SHD_primdef" > "HOL4Prob.boolean_sequence.SHD_primdef"
-  "SHD_def" > "HOL4Prob.boolean_sequence.SHD_def"
-  "SHD_STL_ISO" > "HOL4Prob.boolean_sequence.SHD_STL_ISO"
-  "SHD_SCONST" > "HOL4Prob.boolean_sequence.SHD_SCONST"
-  "SHD_SCONS" > "HOL4Prob.boolean_sequence.SHD_SCONS"
-  "SDROP_def" > "HOL4Prob.boolean_sequence.SDROP_def"
-  "SDEST_primdef" > "HOL4Prob.boolean_sequence.SDEST_primdef"
-  "SDEST_def" > "HOL4Prob.boolean_sequence.SDEST_def"
-  "SCONS_def" > "HOL4Prob.boolean_sequence.SCONS_def"
-  "SCONS_SURJ" > "HOL4Prob.boolean_sequence.SCONS_SURJ"
-  "SCONST_primdef" > "HOL4Prob.boolean_sequence.SCONST_primdef"
-  "SCONST_def" > "HOL4Prob.boolean_sequence.SCONST_def"
-
-end