isabelle: Changelog

smolkas [Wed, 02 Jan 2013 20:52:39 +0100] rev 50679

removed whitespace

smolkas [Wed, 02 Jan 2013 20:52:32 +0100] rev 50678

removed duplicate code

smolkas [Wed, 02 Jan 2013 20:35:49 +0100] rev 50677

use rpair to avoid swap

blanchet [Wed, 02 Jan 2013 19:59:06 +0100] rev 50676

generate "obtain" steps corresponding to skolemization inferences

blanchet [Wed, 02 Jan 2013 16:32:40 +0100] rev 50675

keep E's and Vampire's skolemization steps

blanchet [Wed, 02 Jan 2013 16:02:33 +0100] rev 50674

tuning

blanchet [Wed, 02 Jan 2013 15:54:38 +0100] rev 50673

fixed oversensitive Skolem handling (cf. eaa540986291)

blanchet [Wed, 02 Jan 2013 15:44:00 +0100] rev 50672

added "obtain" to Isar proof construction data structure

blanchet [Wed, 02 Jan 2013 13:31:13 +0100] rev 50671

tuning

blanchet [Wed, 02 Jan 2013 13:14:47 +0100] rev 50670

properly take the existential closure of skolems

isabelle