metit

　Paulson 教授の MetiTarski の組み込みは当然 Isabelle が最初になると思っていたのですが，13日に更新されたNASAのPVSライブラリー

http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/nasalib-6.0.5-full.tgz

に先を越されてしまいました．出所はお弟子さん，ソルバーも Z3 だけなので，まぁ余裕と言った所なのかも知れませんが．．．