blanchet [Tue, 24 Jun 2014 08:20:00 +0200] rev 58637
changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
blanchet [Tue, 24 Jun 2014 08:19:58 +0200] rev 58636
use strings to communicate with external process, to ease debugging
blanchet [Tue, 24 Jun 2014 08:19:57 +0200] rev 58635
added 'dummy_thf_ml' prover for experiments with HOLyHammer
blanchet [Tue, 24 Jun 2014 08:19:56 +0200] rev 58634
phantoms may also occur in THF1
blanchet [Tue, 24 Jun 2014 08:19:55 +0200] rev 58633
added experimental MaSh engine
blanchet [Tue, 24 Jun 2014 08:19:55 +0200] rev 58632
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
blanchet [Tue, 24 Jun 2014 08:19:54 +0200] rev 58631
help reconstruction of Z3 skolemization by weakening formulas a bit
blanchet [Tue, 24 Jun 2014 08:19:22 +0200] rev 58630
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet [Tue, 24 Jun 2014 08:19:22 +0200] rev 58629
given two one-liners, only show the best of the two
blanchet [Tue, 24 Jun 2014 08:19:22 +0200] rev 58628
don't generate Isar proof skeleton for what amounts to a one-line proof