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/Tools/find_theorems.ML
Sun, 20 Mar 2011 21:28:11 +0100 wenzelm structure Timing: covers former start_timing/end_timing and Output.timeit etc; file | diff | annotate
Fri, 25 Feb 2011 16:57:44 +0100 krauss reactivate time measurement (partly reverting c27b0b37041a); file | diff | annotate
Fri, 25 Feb 2011 16:57:43 +0100 krauss generalize find_theorems filters to work on raw propositions, too file | diff | annotate
Fri, 25 Feb 2011 12:16:18 +0100 noschinl Refactor find_theorems to provide a more general filter_facts method file | diff | annotate
Wed, 23 Feb 2011 17:40:28 +0100 noschinl fix non-exhaustive pattern match in find_theorems file | diff | annotate
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; file | diff | annotate
Wed, 11 Aug 2010 18:03:02 +0200 wenzelm misc tuning and simplification; file | diff | annotate
Wed, 11 Aug 2010 17:50:29 +0200 wenzelm simplified/unified command setup; file | diff | annotate
Sat, 15 May 2010 23:40:00 +0200 wenzelm renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time; file | diff | annotate
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse; file | diff | annotate
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic; file | diff | annotate
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord; file | diff | annotate
Mon, 14 Dec 2009 16:35:00 +0100 haftmann avoid negative indices as argument ot drop file | diff | annotate
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop file | diff | annotate
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop file | diff | annotate
Sun, 29 Nov 2009 12:56:30 +1100 kleing Expand nested abbreviations before applying dummy patterns. file | diff | annotate
Mon, 02 Nov 2009 19:56:06 +0100 wenzelm observe usual naming conventions; file | diff | annotate
Mon, 02 Nov 2009 16:44:18 +0100 krauss find_theorems: respect conceal flag file | diff | annotate
Thu, 29 Oct 2009 11:56:02 +0100 wenzelm less hermetic ML; file | diff | annotate
Wed, 28 Oct 2009 22:02:53 +0100 wenzelm renamed Proof.flat_goal to Proof.simple_goal; file | diff | annotate
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics; file | diff | annotate
Wed, 21 Oct 2009 08:16:25 +0200 haftmann merged file | diff | annotate
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix file | diff | annotate
Tue, 20 Oct 2009 16:13:01 +0200 haftmann replaced old_style infixes eq_set, subset, union, inter and variants by generic versions file | diff | annotate
Wed, 21 Oct 2009 16:41:22 +1100 kleing find_theorems: better handling of abbreviations (by Timothy Bourke) file | diff | annotate
Tue, 20 Oct 2009 20:54:31 +0200 wenzelm uniform use of Integer.min/max; file | diff | annotate
Fri, 02 Oct 2009 22:02:11 +0200 wenzelm replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools; file | diff | annotate
Thu, 01 Oct 2009 00:32:00 +0200 wenzelm misc tuning and simplification; file | diff | annotate
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref; file | diff | annotate
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset; file | diff | annotate
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.; file | diff | annotate
Wed, 17 Jun 2009 17:07:26 +0200 wenzelm more detailed start_timing/end_timing; file | diff | annotate
Wed, 17 Jun 2009 15:14:48 +0200 wenzelm minor tuning according to Isabelle/ML conventions; file | diff | annotate
Wed, 06 May 2009 10:55:47 +1000 Timothy Bourke Prototype introiff option for find_theorems. file | diff | annotate
Tue, 31 Mar 2009 20:40:25 +0200 wenzelm superficial tuning; file | diff | annotate
Mon, 30 Mar 2009 12:25:52 +1100 Timothy Bourke Limit the number of results returned by auto_solves. file | diff | annotate
Tue, 24 Mar 2009 15:55:11 +1100 Timothy Bourke Use assms rather than prems in find_theorems solves. file | diff | annotate
Thu, 12 Mar 2009 15:54:58 +0100 wenzelm Assumption.all_prems_of, Assumption.all_assms_of; file | diff | annotate
Sun, 08 Mar 2009 17:26:14 +0100 wenzelm moved basic algebra of long names from structure NameSpace to Long_Name; file | diff | annotate
Fri, 06 Mar 2009 22:32:27 +0100 wenzelm replaced archaic use of rep_ss by Simplifier.mksimps; file | diff | annotate
Wed, 04 Mar 2009 00:05:20 +0100 wenzelm renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts); file | diff | annotate
Tue, 03 Mar 2009 14:54:12 +0100 wenzelm nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses; file | diff | annotate
Sun, 01 Mar 2009 16:22:37 +0100 wenzelm avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example; file | diff | annotate
Sun, 01 Mar 2009 14:45:23 +0100 wenzelm replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already); file | diff | annotate
Fri, 27 Feb 2009 16:05:40 +0100 wenzelm observe basic Isabelle/ML coding conventions; file | diff | annotate
Fri, 27 Feb 2009 15:46:22 +0100 wenzelm moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each; file | diff | annotate | base
less more (0) tip
isabelle