src/HOL/Tools/Function/function_common.ML
Sun, 16 Jun 2013 22:56:44 +0200 krauss export dom predicate in the info record
Sun, 16 Jun 2013 01:39:00 +0200 krauss export cases rule in the info record
Sun, 28 Oct 2012 02:22:39 +0000 Christian Urban added function store_termination_rule to the signature, as it is used in Nominal2
Sun, 21 Oct 2012 22:31:39 +0200 wenzelm removed dead code;
Sun, 21 Oct 2012 22:12:22 +0200 wenzelm proper signatures;
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser;
Wed, 15 Feb 2012 22:44:31 +0100 wenzelm discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
less more (0) -30 -10 -7 tip