| Wed, 26 Jun 2013 11:54:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 18:23:46 +0200 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 22:47:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 16:43:32 +0100 |
wenzelm |
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 17:45:04 +0100 |
wenzelm |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 17:00:23 +0100 |
wenzelm |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 23:55:53 +0100 |
wenzelm |
more general Proof_Context.bind_propp, which allows outer parameters;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:51:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:23:41 +0100 |
wenzelm |
tuned signature -- canonical argument order;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2011 20:20:49 +0200 |
wenzelm |
eliminated slightly odd Proof_Context.bind_fixes;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 23:02:43 +0200 |
wenzelm |
more precise positions via binding;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 21:50:04 +0200 |
wenzelm |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 19:55:42 +0200 |
wenzelm |
more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 17:58:45 +0200 |
wenzelm |
reorganized fixes as specialized (global) name space;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 12:46:18 +0200 |
wenzelm |
tuned signature, disentangled dependencies;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Mon, 30 Aug 2010 15:19:39 +0200 |
wenzelm |
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| 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
|
| 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
|
| Fri, 05 May 2000 22:09:41 +0200 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Thu, 30 Mar 2000 14:24:46 +0200 |
wenzelm |
ProofContext.find_free;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2000 00:18:54 +0100 |
wenzelm |
handle general case: params and hyps of thesis;
|
file |
diff |
annotate
|
| Thu, 06 Jan 2000 16:00:18 +0100 |
wenzelm |
obtain: renamed 'in' to 'where';
|
file |
diff |
annotate
|
| Wed, 05 Jan 2000 11:45:01 +0100 |
wenzelm |
ObtainFun;
|
file |
diff |
annotate
|
| Fri, 22 Oct 1999 21:48:50 +0200 |
wenzelm |
warn_extra_tfrees;
|
file |
diff |
annotate
|
| Fri, 01 Oct 1999 20:38:16 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Fri, 01 Oct 1999 20:36:53 +0200 |
wenzelm |
The 'obtain' language element -- achieves (eliminated) existential
|
file |
diff |
annotate
|