| Sun, 03 May 2015 16:44:38 +0200 |
wenzelm |
suppress formal sort-constraints, in accordance to norm_hhf_eqs;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2015 23:35:41 +0100 |
wenzelm |
added Proof_Context.cterm_of/ctyp_of convenience;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 14:57:06 +0100 |
wenzelm |
added 'print_defn_rules' command;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 20:05:17 +0200 |
wenzelm |
clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:21:33 +0200 |
wenzelm |
normalize defs (again, cf. 008b7858f3c0);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:51:01 +0200 |
wenzelm |
retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;
|
file |
diff |
annotate
|
| Sat, 31 Mar 2012 19:09:59 +0200 |
wenzelm |
more direct Local_Defs.contract;
|
file |
diff |
annotate
|
| Sat, 31 Mar 2012 15:29:49 +0200 |
wenzelm |
more precise Local_Defs.expand wrt. *local* prems only;
|
file |
diff |
annotate
|
| Wed, 21 Mar 2012 11:00:34 +0100 |
wenzelm |
prefer explicitly qualified exception List.Empty;
|
file |
diff |
annotate
|
| Wed, 23 Nov 2011 22:59:39 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2011 15:03:11 +0100 |
wenzelm |
more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);
|
file |
diff |
annotate
|
| Tue, 08 Nov 2011 12:20:26 +0100 |
wenzelm |
clarified Local_Defs.export: avoid costly still_fixed test, return all defs;
|
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 20:58:40 +0200 |
wenzelm |
tuned signature -- eliminated odd comment;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 10:31:18 +0200 |
wenzelm |
more uniform Variable.add_frees/add_fixed etc.;
|
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, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 23:54:39 +0200 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 19:47:40 +0200 |
wenzelm |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:41:14 +0100 |
wenzelm |
Local_Defs.contract convenience;
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 23:45:41 +0100 |
wenzelm |
more basic Local_Defs.export_cterm;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:38:46 +0100 |
wenzelm |
modernized structure Primitive_Defs;
|
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
|
| 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
|
| Thu, 12 Mar 2009 15:54:58 +0100 |
wenzelm |
Assumption.all_prems_of, Assumption.all_assms_of;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:38:25 +0100 |
wenzelm |
Thm.def_binding_optional;
|
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
|
| Sun, 11 Jan 2009 14:18:16 +0100 |
haftmann |
stripped Id
|
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 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 18:54:33 +0200 |
wenzelm |
added fixed_abbrev;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 20:57:14 +0200 |
wenzelm |
tuned interfaces;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2007 00:18:06 +0200 |
wenzelm |
added add_def;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 21:10:41 +0200 |
wenzelm |
added export_cterm;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 19:10:23 +0200 |
wenzelm |
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:05:30 +0200 |
wenzelm |
moved ProofContext.pp to Syntax.pp;
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 13:20:19 +0200 |
wenzelm |
PrimitiveDefs.dest/abs_def;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:54 +0200 |
wenzelm |
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:15 +0200 |
wenzelm |
exported meta_rewrite_conv;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:45 +0200 |
wenzelm |
moved conversions to structure Conv;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|