| Sat, 20 Aug 2011 19:21:03 +0200 |
wenzelm |
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 16:06:27 +0200 |
wenzelm |
clarified fulfill_norm_proof: no join_thms yet;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2011 15:56:15 +0200 |
wenzelm |
mark thm tag "kind" as legacy;
|
file |
diff |
annotate
|
| Sat, 15 Jan 2011 12:47:52 +0100 |
berghofe |
unused_thms no longer compares propositions, since this is no longer needed
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:19:48 +0100 |
wenzelm |
standardized split_last/last_elem towards List.last;
|
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, 21 Jul 2010 15:23:46 +0200 |
wenzelm |
thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sat, 08 May 2010 16:53:53 +0200 |
wenzelm |
renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 19:42:54 +0100 |
wenzelm |
unused_thms: show only results from 'theorem(s)' package (via old-style kinds);
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 21:59:35 +0100 |
wenzelm |
unused_thms: ignore kind -- already observes "concealed" flag;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 21:05:47 +0100 |
wenzelm |
structure Thm_Deps;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 19:19:41 +0100 |
wenzelm |
maintain group via name space, not tags;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 14:27:50 +0200 |
wenzelm |
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
|
file |
diff |
annotate
|
| Mon, 28 Sep 2009 20:52:05 +0200 |
wenzelm |
fold_body_thms: pass pthm identifier;
|
file |
diff |
annotate
|
| Mon, 18 May 2009 09:48:06 +0200 |
haftmann |
introduced Thm.generatedK
|
file |
diff |
annotate
|
| Sat, 16 May 2009 20:17:59 +0200 |
bulwahn |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
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
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 21:28:46 +0100 |
wenzelm |
simplified thm_deps -- no need to build a graph datastructure;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 22:12:44 +0100 |
wenzelm |
proof_body/pthm: removed redundant types field;
|
file |
diff |
annotate
|
| Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
file |
diff |
annotate
|
| Sat, 15 Nov 2008 21:31:36 +0100 |
wenzelm |
retrieve thm deps from proof_body;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 11:40:00 +0200 |
wenzelm |
unused_thms: sort_distinct;
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 21:53:05 +0200 |
wenzelm |
removed obsolete BASIC_THM_DEPS;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2008 17:34:15 +0100 |
berghofe |
Added function for finding unused theorems.
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 19:48:06 +0100 |
wenzelm |
thm_deps: sort result;
|
file |
diff |
annotate
|
| Sat, 08 Sep 2007 19:58:38 +0200 |
wenzelm |
Present.session_name;
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Wed, 04 Oct 2006 14:17:38 +0200 |
haftmann |
insert replacing ins ins_int ins_string
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:12:50 +0200 |
wenzelm |
Present.display_graph;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:02 +0100 |
wenzelm |
moved theorem tags from Drule to PureThy;
|
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 22:15:12 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Wed, 03 Aug 2005 16:28:22 +0200 |
berghofe |
Adapted to new argument format of MinProof constructor.
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 20:47:01 +0200 |
wenzelm |
Inttab.defined;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 11:31:32 +0200 |
wenzelm |
File.isatool, File.shell_path;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Tue, 27 Aug 2002 11:06:20 +0200 |
wenzelm |
Thm.proof_of;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2001 17:42:00 +0100 |
berghofe |
Now handles different theorems with same name more gracefully.
|
file |
diff |
annotate
|
| Wed, 17 Oct 2001 18:52:30 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2001 11:04:44 +0200 |
berghofe |
Exchanged % and %%.
|
file |
diff |
annotate
|
| Sat, 01 Sep 2001 00:14:16 +0200 |
wenzelm |
renamed `keep_derivs' to `proofs', and made an integer;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 16:25:53 +0200 |
berghofe |
Adapted to new proof terms.
|
file |
diff |
annotate
|
| Wed, 02 Aug 2000 19:40:14 +0200 |
wenzelm |
adapted deriv;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2000 18:23:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 13 Oct 1999 19:41:35 +0200 |
wenzelm |
system;
|
file |
diff |
annotate
|
| Thu, 07 Oct 1999 15:40:32 +0200 |
berghofe |
Replaced update_new by update.
|
file |
diff |
annotate
|
| Thu, 07 Oct 1999 14:44:55 +0200 |
berghofe |
Added functions for enabling and disabling derivations.
|
file |
diff |
annotate
|
| Thu, 07 Oct 1999 14:32:18 +0200 |
wenzelm |
$ISATOOL;
|
file |
diff |
annotate
|
| Thu, 07 Oct 1999 11:36:39 +0200 |
berghofe |
New function thm_deps for visualizing dependencies of theorems.
|
file |
diff |
annotate
|