Q.MATCH_ABBREV_TAC only uses one parse of its pattern, not all possible parses
Opened this issue · 0 comments
Eric-C-Hall commented
I have attached an example file which explains what I mean (rename it from a .txt file to a .sml file, had to name it that way because it won't let me upload it otherwise, probably because it's afraid of viruses)
qmatch_example_v2Script.txt