src/HOL/Tools/Function/partial_function.ML
Fri, 04 Sep 2015 14:00:13 +0200 wenzelm trim context for persistent storage;
Sun, 26 Jul 2015 17:24:54 +0200 wenzelm updated to infer_instantiate;
Wed, 08 Jul 2015 19:28:43 +0200 wenzelm Variable.focus etc.: optional bindings provided by user;
less more (0) -30 -10 -3 tip