Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
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
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