| Sat, 07 Mar 2009 22:17:25 +0100 |
wenzelm |
more uniform handling of binding in packages;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:11 +0100 |
wenzelm |
use regular Term.add_vars, Term.add_frees etc.;
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 16:30:35 +0100 |
wenzelm |
recovered goal_pat;
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 16:09:12 +0100 |
wenzelm |
inhabitance goal is now stated in original form and result contracted --
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 11:55:46 +0100 |
wenzelm |
add_typedef: unfold set_def in tactical proof as well;
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 10:41:37 +0100 |
wenzelm |
Theory.checkpoint before commencing proof;
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 00:42:52 +0100 |
wenzelm |
misc tuning and modernisation;
|
file |
diff |
annotate
|
| Mon, 08 Dec 2008 08:56:30 +0100 |
krauss |
logically separate typedef axiomatization from constant definition
|
file |
diff |
annotate
|
| Mon, 08 Dec 2008 08:36:16 +0100 |
krauss |
add def before setting up goal
|
file |
diff |
annotate
|
| Sun, 07 Dec 2008 20:41:23 +0100 |
krauss |
killed dead code
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Wed, 19 Nov 2008 08:58:57 +0100 |
haftmann |
explicit inhabitance proof
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:44 +0200 |
haftmann |
tuned typedef interface
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:32 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 13:03:09 +0100 |
wenzelm |
eliminated quiete_mode ref (not really needed);
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:48 +0100 |
haftmann |
interpretation of typedefs
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:07 +0100 |
haftmann |
interpretation for typedefs
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 16:44:20 +0100 |
wenzelm |
ObjectLogic.typedecl;
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:30 +0100 |
haftmann |
separated typedecl module, providing typedecl command with interpretation
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:34 +0200 |
wenzelm |
AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 22:00:15 +0200 |
wenzelm |
tuned Induct interface: prefer pred'' over set'';
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 15:47:01 +0200 |
wenzelm |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 13:20:12 +0200 |
wenzelm |
PrimitiveDefs.mk_defpair;
|
file |
diff |
annotate
|