diff -r 880e587eee9f -r 2d4ea84278da src/HOL/Import/HOL4/Generated/boolean_sequence.imp --- 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