| Mon, 02 Nov 2009 20:57:48 +0100 |
wenzelm |
modernized structure Proof_Display;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:45:23 +0100 |
wenzelm |
modernized structure AutoBind;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:24:45 +0100 |
wenzelm |
modernized structure Rule_Cases;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 22:25:50 +0200 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2009 13:12:54 +0200 |
wenzelm |
Variable.focus: named parameters;
|
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, 24 Jun 2009 21:28:02 +0200 |
wenzelm |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 17:53:33 +0100 |
wenzelm |
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 16:31:16 +0100 |
wenzelm |
replaced add_binds(_i) by bind_terms -- internal version only;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 13:28:55 +0100 |
wenzelm |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 18:32:01 +0100 |
wenzelm |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Wed, 07 Jan 2009 16:22:10 +0100 |
wenzelm |
qed/after_qed: singleton result;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:30 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| 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
|