Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/thm_database.ML
Thu, 27 Apr 2006 15:06:35 +0200 wenzelm tuned basic list operators (flat, maps, map_filter); file | diff | annotate
Sat, 11 Feb 2006 17:17:47 +0100 wenzelm tuned; file | diff | annotate
Mon, 06 Feb 2006 20:58:57 +0100 wenzelm TableFun: renamed xxx_multi to xxx_list; file | diff | annotate
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update; file | diff | annotate
Thu, 01 Sep 2005 18:48:50 +0200 wenzelm curried_lookup/update; file | diff | annotate
Sun, 28 Aug 2005 16:04:54 +0200 wenzelm added (use_)legacy_bindings; file | diff | annotate
Sat, 23 Apr 2005 19:51:54 +0200 wenzelm tuned comment; file | diff | annotate
Thu, 21 Apr 2005 22:02:06 +0200 wenzelm superceded by Pure.thy and CPure.thy; file | diff | annotate
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004 file | diff | annotate
Mon, 26 Apr 2004 15:01:05 +0200 wenzelm use Syntax.is_ascii_identifier; file | diff | annotate
Tue, 02 Jul 2002 15:45:55 +0200 wenzelm removed thms_containing (see pure_thy.ML and proof_context.ML); file | diff | annotate
Mon, 22 Oct 2001 18:04:26 +0200 wenzelm moved goal related stuff to goals.ML; file | diff | annotate
Sun, 14 Oct 2001 22:07:01 +0200 wenzelm added qed_spec_mp etc.; file | diff | annotate
Fri, 31 Aug 2001 16:24:39 +0200 berghofe Exported ml_reserved. file | diff | annotate
Thu, 01 Feb 2001 20:43:14 +0100 wenzelm thms_containing: term args; file | diff | annotate
Tue, 16 Jan 2001 00:35:50 +0100 wenzelm use_text etc.: proper output of error messages; file | diff | annotate
Fri, 12 Jan 2001 20:04:41 +0100 wenzelm use_text_verbose: priority output; file | diff | annotate
Tue, 07 Dec 1999 11:01:48 +0100 nipkow Fixed bug in find-functions: list of parameters must be reversed before file | diff | annotate
Wed, 13 Oct 1999 19:42:12 +0200 wenzelm use_text_verbose; file | diff | annotate
Tue, 05 Oct 1999 16:55:13 +0200 wenzelm fixed ml_store_thm(s): deriv; file | diff | annotate
Sun, 26 Sep 1999 16:38:21 +0200 wenzelm added print_thms_containing; file | diff | annotate
Wed, 22 Sep 1999 20:58:23 +0200 wenzelm ml_store_thm: no warning for ""; file | diff | annotate
Fri, 03 Sep 1999 13:55:46 +0200 wenzelm added no_qed; file | diff | annotate
Wed, 01 Sep 1999 21:09:10 +0200 wenzelm added store/bind_thms; file | diff | annotate
Fri, 06 Aug 1999 11:07:25 +0200 paulson now catches exn THEORY and prints an error message file | diff | annotate
Tue, 09 Mar 1999 12:17:40 +0100 wenzelm Present.theorem; file | diff | annotate
Wed, 03 Feb 1999 17:23:35 +0100 wenzelm open BasicThmDatabase; file | diff | annotate
Fri, 23 Oct 1998 16:44:50 +0200 wenzelm export is_ml_identifier; file | diff | annotate
Thu, 20 Aug 1998 09:25:59 +0200 paulson Now qed_spec_mp respects locales, by calling ml_store_thm file | diff | annotate
Fri, 17 Jul 1998 10:50:28 +0200 paulson added comments file | diff | annotate
Mon, 29 Jun 1998 10:32:06 +0200 wenzelm use_text: verbose flag; file | diff | annotate
Mon, 15 Jun 1998 11:06:00 +0200 wenzelm use_text replaces use_strings; file | diff | annotate
Fri, 09 Jan 1998 14:02:34 +0100 wenzelm thm_ord; file | diff | annotate
Thu, 08 Jan 1998 18:19:48 +0100 wenzelm fixed thm_less; file | diff | annotate
Fri, 19 Dec 1997 09:58:03 +0100 wenzelm adapted to new sort function; file | diff | annotate
Wed, 26 Nov 1997 16:37:43 +0100 wenzelm fixed type of thms_containing; file | diff | annotate
Thu, 30 Oct 1997 10:01:46 +0100 wenzelm tuned; file | diff | annotate
Tue, 28 Oct 1997 17:37:46 +0100 wenzelm restructured -- uses PureThy storage facilities; file | diff | annotate
Fri, 24 Oct 1997 17:19:14 +0200 wenzelm ProtoPure.flexpair_def; file | diff | annotate
Thu, 23 Oct 1997 12:43:07 +0200 wenzelm tuned; file | diff | annotate
Wed, 06 Aug 1997 14:42:44 +0200 wenzelm renamed use_string to use_strings; file | diff | annotate
Wed, 06 Aug 1997 14:12:03 +0200 wenzelm tuned names; file | diff | annotate
Wed, 06 Aug 1997 00:18:34 +0200 berghofe Moved "qed" - functions etc. from thy_read.ML to thm_database.ML. file | diff | annotate
Fri, 01 Nov 1996 15:41:09 +0100 paulson Replaced "sum" (only usage?) by foldl op+ file | diff | annotate
Fri, 17 May 1996 16:22:23 +0200 nipkow Added missing default clause | top_const _ = None; file | diff | annotate
Tue, 09 Apr 1996 12:12:27 +0200 berghofe select_match now sorts list of matching theorems according to the file | diff | annotate
Fri, 15 Mar 1996 12:01:19 +0100 berghofe Added some functions which allow redirection of Isabelle's output file | diff | annotate
Fri, 16 Feb 1996 18:00:47 +0100 paulson Elimination of fully-functorial style. file | diff | annotate
Wed, 25 Oct 1995 13:41:45 +0100 clasohm removed "duplicate" warning from store_thm_db; file | diff | annotate
Fri, 06 Oct 1995 14:43:26 +0100 clasohm changed some comments file | diff | annotate
Wed, 04 Oct 1995 12:59:52 +0100 clasohm added removal of theorems if theory is to be reloaded; changed functions for file | diff | annotate
Fri, 01 Sep 1995 14:25:52 +0200 clasohm fixed bug: duplicate "duplicate" warnings file | diff | annotate
Fri, 01 Sep 1995 13:28:54 +0200 clasohm added cleanup of global simpset to thy_read; file | diff | annotate
Wed, 30 Aug 1995 14:04:39 +0200 clasohm added check for duplicate theorems in theorem database; file | diff | annotate
Fri, 18 Aug 1995 12:28:02 +0200 nipkow fixed bug in findI file | diff | annotate
Mon, 07 Aug 1995 15:23:59 +0200 nipkow Added findI, findEs, and findE. file | diff | annotate
Thu, 01 Jun 1995 13:25:06 +0200 clasohm commented thms_unifying_with out; placed thm_db into signature again; file | diff | annotate
Tue, 30 May 1995 11:57:27 +0200 clasohm removed thm_num and thm_db from signature file | diff | annotate
Tue, 30 May 1995 11:28:13 +0200 clasohm fixed bug in thms_containing; changed error/warning messages; file | diff | annotate
Mon, 29 May 1995 15:04:27 +0200 clasohm changed error message in thms_containing file | diff | annotate
less more (0) tip
isabelle