Lines Matching refs:ALIAS
1090 ("ADD-MACRO-ALIAS" , "ACL2-USER" , "ACL2"),
1092 ("ADD-NTH-ALIAS" , "ACL2-USER" , "ACL2"),
2354 ("REMOVE-MACRO-ALIAS" , "ACL2-USER" , "ACL2"),
2356 ("REMOVE-NTH-ALIAS" , "ACL2-USER" , "ACL2"),
3003 ("ADD-MACRO-ALIAS" , "U" , "ACL2"),
3005 ("ADD-NTH-ALIAS" , "U" , "ACL2"),
4260 ("REMOVE-MACRO-ALIAS" , "U" , "ACL2"),
4262 ("REMOVE-NTH-ALIAS" , "U" , "ACL2"),
4839 ("ADD-MACRO-ALIAS" , "ACL2-ASG" , "ACL2"),
4841 ("ADD-NTH-ALIAS" , "ACL2-ASG" , "ACL2"),
6103 ("REMOVE-MACRO-ALIAS" , "ACL2-ASG" , "ACL2"),
6105 ("REMOVE-NTH-ALIAS" , "ACL2-ASG" , "ACL2"),
6688 ("ADD-MACRO-ALIAS" , "ACL2-AGP" , "ACL2"),
6690 ("ADD-NTH-ALIAS" , "ACL2-AGP" , "ACL2"),
7952 ("REMOVE-MACRO-ALIAS" , "ACL2-AGP" , "ACL2"),
7954 ("REMOVE-NTH-ALIAS" , "ACL2-AGP" , "ACL2"),
8537 ("ADD-MACRO-ALIAS" , "ACL2-CRG" , "ACL2"),
8539 ("ADD-NTH-ALIAS" , "ACL2-CRG" , "ACL2"),
9801 ("REMOVE-MACRO-ALIAS" , "ACL2-CRG" , "ACL2"),
9803 ("REMOVE-NTH-ALIAS" , "ACL2-CRG" , "ACL2"),