| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
renamed ML file and module
|
file |
diff |
annotate
| base
|
| Thu, 04 Jun 2009 16:11:04 +0200 |
haftmann |
avoid Library.foldl_map
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:42:19 +0100 |
wenzelm |
explicit Binding.qualified_name -- prevents implicitly qualified bstring;
|
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
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
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:17 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:03 +0100 |
wenzelm |
simplified PureThy.store_thm;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:09:20 +0100 |
haftmann |
more antiquotations
|
file |
diff |
annotate
|
| Mon, 29 Oct 2007 16:13:41 +0100 |
wenzelm |
qualified Proofterm.proofs;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 15:34:35 +0200 |
wenzelm |
simplified interpretation setup;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:26 +0200 |
wenzelm |
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:14 +0200 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:47 +0200 |
wenzelm |
Thm.fold_terms;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:33 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:11:03 +0200 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:37 +0200 |
wenzelm |
removed obsolete Drule.frees/vars_of etc.;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:16:54 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:28 +0200 |
wenzelm |
renamed Type.(un)varifyT to Logic.(un)varifyT;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:54 +0100 |
wenzelm |
Envir.(beta_)eta_contract;
|
file |
diff |
annotate
|
| Tue, 06 Dec 2005 09:04:09 +0100 |
haftmann |
re-oriented some result tuples in PureThy
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:38 +0200 |
wenzelm |
OldGoals;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 16:17:34 +0200 |
haftmann |
introduced AList module in favor of assoc etc.
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:14 +0200 |
wenzelm |
Theory.restore_naming;
|
file |
diff |
annotate
|