Fri, 15 Feb 2013 13:54:54 +0100 annotate obtains with types
blanchet [Fri, 15 Feb 2013 13:54:54 +0100] rev 51158
annotate obtains with types
Fri, 15 Feb 2013 13:43:06 +0100 merge
blanchet [Fri, 15 Feb 2013 13:43:06 +0100] rev 51157
merge
Fri, 15 Feb 2013 13:37:37 +0100 made check for conjecture skolemization sound
blanchet [Fri, 15 Feb 2013 13:37:37 +0100] rev 51156
made check for conjecture skolemization sound
Fri, 15 Feb 2013 13:29:37 +0100 use safe var index
smolkas [Fri, 15 Feb 2013 13:29:37 +0100] rev 51155
use safe var index
Fri, 15 Feb 2013 12:16:24 +0100 merged
Andreas Lochbihler [Fri, 15 Feb 2013 12:16:24 +0100] rev 51154
merged
Fri, 15 Feb 2013 11:02:34 +0100 more type class instances for Numeral_Type (contributed by Jesus Aransay)
Andreas Lochbihler [Fri, 15 Feb 2013 11:02:34 +0100] rev 51153
more type class instances for Numeral_Type (contributed by Jesus Aransay)
Fri, 15 Feb 2013 10:52:47 +0100 added lemma
Andreas Lochbihler [Fri, 15 Feb 2013 10:52:47 +0100] rev 51152
added lemma
Fri, 15 Feb 2013 12:10:09 +0100 merge
blanchet [Fri, 15 Feb 2013 12:10:09 +0100] rev 51151
merge
Fri, 15 Feb 2013 11:36:34 +0100 merge
blanchet [Fri, 15 Feb 2013 11:36:34 +0100] rev 51150
merge
Fri, 15 Feb 2013 11:27:15 +0100 skolemize conjecture properly in Isar proof
blanchet [Fri, 15 Feb 2013 11:27:15 +0100] rev 51149
skolemize conjecture properly in Isar proof
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip