Wed, 25 Jul 2001 18:21:01 +0200 defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some
paulson [Wed, 25 Jul 2001 18:21:01 +0200] rev 11455
defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some dynamically, so recdef no longer needs to import Hilbert_Choice.
Wed, 25 Jul 2001 17:58:26 +0200 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson [Wed, 25 Jul 2001 17:58:26 +0200] rev 11454
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
Wed, 25 Jul 2001 13:44:32 +0200 partial restructuring to reduce dependence on Axiom of Choice
paulson [Wed, 25 Jul 2001 13:44:32 +0200] rev 11453
partial restructuring to reduce dependence on Axiom of Choice
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip