2016-06-20 情報検索 Isabelle ダメ出し 情報検索の機能が低い。find_* とか print_* だけ。小洒落た機能はない。キーワード(コマンド名)に対して、そのコマンドがどのセオリーやどのMLファイルに由来するかも検索できないようだ。ディレクトリ内からファイルを探してソース読むしか無いようだ。shellコマンド、findとgrepの出番です、って、なんだよもう。