src/HOL/Tools/datatype_realizer.ML
Tue, 31 May 2005 11:53:14 +0200 wenzelm Theory.restore_naming;
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Tue, 26 Oct 2004 16:25:41 +0200 berghofe Fixed problem with sorts in function make_casedists.
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Wed, 27 Nov 2002 17:06:47 +0100 berghofe Changed format of realizers / correctness proofs.
Wed, 13 Nov 2002 15:28:41 +0100 berghofe prove_goal' -> Goal.simple_prove_goal_cterm
Mon, 21 Oct 2002 16:57:39 +0200 berghofe Changed type of Logic.strip_horn.
Thu, 10 Oct 2002 14:26:50 +0200 berghofe Reimplemented parts of datatype package dealing with datatypes involving
Wed, 07 Aug 2002 16:46:15 +0200 berghofe Module for defining realizers for induction and case analysis theorems
less more (0) tip