I want to prove ``a <> b`` for some a,b. After stripping I am asked to
prove F. I was able to use the assumptions to prove ``F = T``. At this
point I thought "asm_simp_tac bool_ss []" should finish the proof but it
doesn't. So "pop_assum (fn th => rewrite_tac [th]" actually finished the
work for
SECOND CALL FOR PAPERS
LSFA 2019
14th Workshop on Logical and Semantic Frameworks, with Applications
24-26 August 2019, Natal, Brazil
https://sites.google.com/view/lsfa2019
Logical and semantic frameworks are formal languages used to represent
logics, languages and systems. These frameworks
Second Call for Papers
SEFM 2019
17th International Conference on Software Engineering and Formal Methods
Oslo, Norway, September 16-20, 2019