2011-05-23 blanchet pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
2011-05-23 hoelzl move lemmas to Extended_Reals and Extended_Real_Limits
2011-05-23 krauss separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
2011-05-22 krauss reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
2011-05-22 krauss fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
2011-05-22 blanchet added message when Waldmeister isn't run
Loading...
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip