| Tue, 03 Apr 2007 19:24:13 +0200 |
wenzelm |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:19:03 +0100 |
wenzelm |
export: added explicit term operation;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:29 +0100 |
wenzelm |
qualified MetaSimplifier.norm_hhf(_protect);
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 19:39:50 +0100 |
wenzelm |
moved statement to specification.ML;
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 21:39:31 +0200 |
wenzelm |
statement: Variable.fix_frees;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:27:02 +0200 |
wenzelm |
added tactical result;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:01 +0200 |
wenzelm |
moved basic assumption operations from structure ProofContext to Assumption;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:41 +0200 |
wenzelm |
Variable.import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:08 +0200 |
wenzelm |
added find_free (from term.ML);
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:11 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:55 +0200 |
wenzelm |
guess: proper context for polymorphic parameters;
|
file |
diff |
annotate
|
| Mon, 03 Jul 2006 19:33:09 +0200 |
wenzelm |
obtain_export: Thm.generalize;
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:37:47 +0200 |
wenzelm |
Term.internal;
|
file |
diff |
annotate
|
| Thu, 15 Jun 2006 23:08:54 +0200 |
wenzelm |
ProofContext: moved variable operations to struct Variable;
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 21:59:24 +0200 |
wenzelm |
fixes: include mixfix syntax;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 21:54:25 +0200 |
wenzelm |
guess: more careful about local polymorphism;
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:22:05 +0200 |
wenzelm |
removed 'concl is' patterns;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:07 +0100 |
wenzelm |
subtract (op =);
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 16:31:35 +0100 |
wenzelm |
Proof.refine_insert;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 12:52:24 +0100 |
wenzelm |
obtain(_i): optional name for 'that';
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 18:19:25 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:32 +0100 |
wenzelm |
ProofContext.inferred_param;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2006 19:58:56 +0100 |
wenzelm |
guess: used fixed inferred_type of vars;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:11 +0100 |
wenzelm |
uniform handling of fixes;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:34:04 +0100 |
wenzelm |
generic attributes;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:31 +0100 |
wenzelm |
Term.betapplys;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:21 +0100 |
wenzelm |
guess: Seq.hd;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 10:44:40 +0100 |
wenzelm |
simplified after_qed;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:28:12 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:54 +0200 |
wenzelm |
improved check_result;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:24 +0200 |
wenzelm |
tuned error msg;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:08:07 +0200 |
wenzelm |
added 'guess', which derives the obtained context from the course of reasoning;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:42 +0200 |
wenzelm |
tuned Isar proof elements;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 11:17:46 +0200 |
wenzelm |
prepare attributes here;
|
file |
diff |
annotate
|
| Mon, 08 Aug 2005 22:14:04 +0200 |
ballarin |
After_qed takes result argument.
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 11:16:34 +0200 |
haftmann |
(intermediate commit)
|
file |
diff |
annotate
|
| Wed, 29 Jun 2005 15:13:36 +0200 |
wenzelm |
no Syntax.internal on thesis;
|
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
|
| Wed, 27 Feb 2002 21:53:33 +0100 |
wenzelm |
improved messages;
|
file |
diff |
annotate
|
| Thu, 06 Dec 2001 00:43:03 +0100 |
wenzelm |
Syntax.internal thesis;
|
file |
diff |
annotate
|
| Mon, 03 Dec 2001 21:31:55 +0100 |
wenzelm |
renamed rule_context.ML to context_rules.ML;
|
file |
diff |
annotate
|
| Thu, 29 Nov 2001 01:51:06 +0100 |
wenzelm |
RuleContext.intro_query_local;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2001 21:35:21 +0100 |
wenzelm |
Proof.have_i: multiple statements;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2001 20:59:35 +0100 |
wenzelm |
pretty/print functions with context;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2001 18:02:50 +0200 |
wenzelm |
improved source arrangement of obtain;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2001 23:02:14 +0200 |
wenzelm |
simplified exporter interface;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:09:19 +0200 |
wenzelm |
use ObjectLogic;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2001 20:45:11 +0100 |
wenzelm |
comment
|
file |
diff |
annotate
|
| Mon, 04 Dec 2000 23:18:07 +0100 |
wenzelm |
fixed binding of parameters;
|
file |
diff |
annotate
|
| Mon, 13 Nov 2000 22:01:07 +0100 |
wenzelm |
tuned statement args;
|
file |
diff |
annotate
|
| Fri, 03 Nov 2000 21:27:06 +0100 |
wenzelm |
improved handling of "that": insert into goal, only declare as Pure "intro";
|
file |
diff |
annotate
|
| Mon, 31 Jul 2000 14:37:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2000 12:54:07 +0200 |
wenzelm |
turned into plain context element;
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 11:39:22 +0200 |
wenzelm |
bind_skolem;
|
file |
diff |
annotate
|