1open HolKernel Parse boolLib bossLib intSyntax pairSyntax listSyntax stringLib numLib sexp; 2 3val package = 4 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil))))); 5 6val events = [ 7 8(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 9mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" 10"NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym 11"COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 12mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "T") ( 13mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 14mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair (mksym "COMMON-LISP" 15"CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair ( 16mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 17"ACL2" "SUBSET") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym 18"ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym 19"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 20mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 21"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 22, 23 24(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-INTERSECT") ( 25mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 26"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 27mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym 28"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 29mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 30mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair ( 31mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym 32"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 33mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mkpair (mksym 34"COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 35mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mkpair (mksym 36"COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) ( 37mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 38"NIL")))) (mkpair (mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mkpair ( 39mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 40"NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym 41"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" 42"NIL"))))) 43, 44 45(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-UNION") ( 46mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 47"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 48mkpair (mksym "COMMON-LISP" "ENDP") (mkpair (mksym "ACL2" "X") (mksym 49"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mkpair (mkpair (mksym 50"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "MEMBERP") (mkpair (mkpair ( 51mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" 52"NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 53mkpair (mksym "ACL2" "SET-UNION") (mkpair (mkpair (mksym "COMMON-LISP" "CDR") ( 54mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" 55"Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" 56"CONS") (mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "X") ( 57mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "SET-UNION") ( 58mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym 59"COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 60mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))) (mksym 61"COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 62, 63 64(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "SET-EQUAL") ( 65mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 66"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 67mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym 68"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 69"SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") (mksym 70"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 71mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 72"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 73, 74 75(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "SUBSET-IS-REFLEXIVE") ( 76mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair ( 77mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 78, 79 80(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "SUBSET-IS-TRANSITIVE") ( 81mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 82"IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") ( 83mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 84mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "Z") ( 85mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 86mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 87"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 88mksym "ACL2" "X") (mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP" "NIL")))) ( 89mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 90, 91 92(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 93"SUBSET-OF-EMPTY-IS-EMPTY") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 94mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 95mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") ( 96mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair ( 97mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") ( 98mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") ( 99mkpair (mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym 100"COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair ( 101mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "Y") (mksym 102"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 103"NIL")))) (mksym "COMMON-LISP" "NIL")))) 104, 105 106(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 107"SET-EQUAL-IS-AN-EQUIVALENCE") (mkpair (mkpair (mksym "COMMON-LISP" "IF") ( 108mkpair (mkpair (mksym "ACL2" "BOOLEANP") (mkpair (mkpair (mksym "ACL2" 109"SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 110"COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym 111"COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym 112"ACL2" "X") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 113mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 114mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair ( 115mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 116"ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "X") ( 117mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 118mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 119mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mksym 120"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" 121"SET-EQUAL") (mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "Z") (mksym 122"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 123mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 124"NIL"))))) (mkpair (mkpair (mksym "ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" 125"X") (mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP" "NIL")))) (mksym 126"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 127mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 128"NIL"))))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 129"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 130mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 131"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mksym 132"COMMON-LISP" "NIL")))) 133, 134 135(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 136"SUBSET-IS-ANTISYMMETRIC") (mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair ( 137mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" "SUBSET") ( 138mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" 139"NIL")))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "Y") ( 140mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair ( 141mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" "NIL") (mksym 142"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (mkpair (mksym 143"ACL2" "SET-EQUAL") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") ( 144mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) (mksym 145"COMMON-LISP" "NIL")))) 146, 147 148(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 149"INTERSECT-IS-A-SUBSET-1") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 150mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mksym "ACL2" "X") (mkpair ( 151mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "X") ( 152mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 153, 154 155(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 156"INTERSECT-IS-A-SUBSET-2") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 157mkpair (mksym "ACL2" "SET-INTERSECT") (mkpair (mksym "ACL2" "X") (mkpair ( 158mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mksym "ACL2" "Y") ( 159mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) 160, 161 162(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "UNION-IS-A-SUBSET-1") ( 163mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair ( 164mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" "X") (mkpair (mksym 165"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 166mksym "COMMON-LISP" "NIL")))) 167, 168 169(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "UNION-IS-A-SUBSET-2") ( 170mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "Y") (mkpair ( 171mkpair (mksym "ACL2" "SET-UNION") (mkpair (mksym "ACL2" "X") (mkpair (mksym 172"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 173mksym "COMMON-LISP" "NIL")))) 174, 175 176(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 177"SUPERSET-CONTAINS-EVERYTHING") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 178mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 179"MEMBERP") (mkpair (mksym "ACL2" "E") (mkpair (mksym "ACL2" "X") (mksym 180"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 181mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 182mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 183"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 184mkpair (mksym "ACL2" "MEMBERP") (mkpair (mksym "ACL2" "E") (mkpair (mksym 185"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 186mksym "COMMON-LISP" "NIL")))) 187, 188 189(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "SUBSET-OF-NIL-IS-NIL") ( 190mkpair (mkpair (mksym "ACL2" "IMPLIES") (mkpair (mkpair (mksym "COMMON-LISP" 191"IF") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym 192"COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL"))) ( 193mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair ( 194mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) ( 195mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym "COMMON-LISP" 196"NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) (mkpair ( 197mkpair (mksym "COMMON-LISP" "NOT") (mkpair (mkpair (mksym "COMMON-LISP" 198"CONSP") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym 199"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 200"NIL")))) 201, 202 203(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "PROPER-SUBSET") ( 204mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 205"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair ( 206mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym 207"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym 208"COMMON-LISP" "NOT") (mkpair (mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym 209"ACL2" "Y") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym 210"COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair ( 211mksym "COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" 212"NIL"))))) (mksym "COMMON-LISP" "NIL"))))) 213, 214 215(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 216"PROPER-SUBSET-IS-IRREFLEXIVE") (mkpair (mkpair (mksym "COMMON-LISP" "NOT") ( 217mkpair (mkpair (mksym "ACL2" "PROPER-SUBSET") (mkpair (mksym "ACL2" "X") ( 218mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 219"NIL"))) (mksym "COMMON-LISP" "NIL")))) 220, 221 222(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 223"PROPER-SUBSET-IS-TRANSITIVE") (mkpair (mkpair (mksym "ACL2" "IMPLIES") ( 224mkpair (mkpair (mksym "COMMON-LISP" "IF") (mkpair (mkpair (mksym "ACL2" 225"PROPER-SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym 226"COMMON-LISP" "NIL")))) (mkpair (mkpair (mksym "ACL2" "PROPER-SUBSET") ( 227mkpair (mksym "ACL2" "Y") (mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP" 228"NIL")))) (mkpair (mkpair (mksym "COMMON-LISP" "QUOTE") (mkpair (mksym 229"COMMON-LISP" "NIL") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))))) ( 230mkpair (mkpair (mksym "ACL2" "PROPER-SUBSET") (mkpair (mksym "ACL2" "X") ( 231mkpair (mksym "ACL2" "Z") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" 232"NIL")))) (mksym "COMMON-LISP" "NIL")))) 233, 234 235(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" 236"PROPER-SUBSET-IS-STRONGER-THAN-SUBSET") (mkpair (mkpair (mksym "ACL2" 237"IMPLIES") (mkpair (mkpair (mksym "ACL2" "PROPER-SUBSET") (mkpair (mksym 238"ACL2" "X") (mkpair (mksym "ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mkpair ( 239mkpair (mksym "ACL2" "SUBSET") (mkpair (mksym "ACL2" "X") (mkpair (mksym 240"ACL2" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))) ( 241mksym "COMMON-LISP" "NIL")))) 242 243]; 244