| Fri, 23 Aug 2013 20:35:50 +0200 |
wenzelm |
added Theory.setup convenience;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 13:12:54 +0200 |
wenzelm |
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
|
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
|
| Sun, 26 Aug 2012 22:23:10 +0200 |
wenzelm |
entity markup for theory Pure, to enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
| Wed, 01 Aug 2012 19:53:20 +0200 |
wenzelm |
more standard bootstrapping of Pure.thy;
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 22:48:38 +0100 |
wenzelm |
eliminated odd 'finalconsts' / Theory.add_finals;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2011 16:32:29 +0100 |
wenzelm |
prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:05:53 +0200 |
wenzelm |
explicit join_syntax ensures command transaction integrity of 'theory';
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 13:54:07 +0200 |
wenzelm |
added Theory.nodes_of convenience;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 15:01:50 +0200 |
wenzelm |
recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 14:05:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:44:39 +0200 |
wenzelm |
pass plain Proof.context for pretty printing;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2011 11:13:29 +0200 |
wenzelm |
simplified pretty printing context, which is only required for certain kernel operations;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 22:47:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
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
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 17:36:32 +0100 |
wenzelm |
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 16:01:45 +0100 |
wenzelm |
disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 15:20:31 +0100 |
wenzelm |
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 00:51:18 +0100 |
wenzelm |
replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
|
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
|
| Mon, 04 Jan 2010 23:20:35 +0100 |
wenzelm |
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
|
file |
diff |
annotate
|
| Mon, 04 Jan 2010 14:09:56 +0100 |
haftmann |
dropped copy operation for legacy TheoryDataFun
|
file |
diff |
annotate
|
| Sun, 15 Nov 2009 20:39:22 +0100 |
wenzelm |
primitive defs: clarified def (axiom name) vs. description;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 19:19:29 +0100 |
wenzelm |
begin_theory: set theory_name here;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 13:04:06 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 20:54:08 +0200 |
wenzelm |
maintain explicit name space kind;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:20:03 +0200 |
wenzelm |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
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:27:20 +0200 |
wenzelm |
removed redundant Sign.certify_prop, use Sign.cert_prop instead;
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 11:10:02 +0100 |
wenzelm |
renamed NameSpace.bind to NameSpace.define;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 12:07:30 +0100 |
wenzelm |
Theory.add_axioms/add_defs: replaced old bstring by binding;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 15:09:08 +0100 |
wenzelm |
Binding.str_of;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:32 +0100 |
haftmann |
binding is alias for Binding.T
|
file |
diff |
annotate
|
| Sat, 13 Dec 2008 15:00:40 +0100 |
wenzelm |
requires: check ancestors directly;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2008 18:42:37 +0100 |
haftmann |
removed Table.extend, NameSpace.extend_table
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:47:35 +0200 |
wenzelm |
simplified specify_const: canonical args, global deps;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
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
|
| Tue, 15 Apr 2008 18:49:23 +0200 |
wenzelm |
removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:45 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 19:45:56 +0200 |
wenzelm |
apply_wrappers: perhaps_apply/loop;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2007 17:16:40 +0200 |
wenzelm |
Theory.specify_const: added deps argument;
|
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:39 +0200 |
wenzelm |
added specify_const;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 21:39:48 +0200 |
wenzelm |
Sign.the_const_constraint;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 13:28:41 +0200 |
wenzelm |
Syntax.parse/check/read;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 20:56:34 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|