src/Pure/theory.ML
2017-04-19 wenzelm 2017-04-19 proper base name, e.g. relevant for Code_Namespace.hierarchical_program;
2016-11-07 wenzelm 2016-11-07 unused since 15865e0c5598;
2016-07-05 wenzelm 2016-07-05 PIDE reports of implicit variable scope;
2016-04-25 wenzelm 2016-04-25 more rigid check of lhs;
2016-04-24 wenzelm 2016-04-24 within a proof body context, undeclared frees are like global constants; tuned signature;
2015-12-28 wenzelm 2015-12-28 suppress irrelevant position reports;
2015-09-25 wenzelm 2015-09-25 tuned signature: eliminated pointless type Context.pretty;
2015-09-24 wenzelm 2015-09-24 more explicit Defs.context: use proper name spaces as far as possible;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 eliminated separate type Theory.dep: use typeargs uniformly for consts/types; Object_Logic.add_judgment more like Theory.specify_const;
2015-09-22 wenzelm 2015-09-22 renamed Defs.node to Defs.item; clarified type Defs.item; clarified item_ord for printing;
2015-09-22 wenzelm 2015-09-22 tuned signature;
2015-09-22 wenzelm 2015-09-22 tuned whitespace;
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2015-08-28 wenzelm 2015-08-28 more abstract theory certificate, which is not necessarily the full theory;
2015-08-16 wenzelm 2015-08-16 prefer theory_id operations; tuned signature;
2015-04-16 wenzelm 2015-04-16 formal Theory.check, with markup and completion;
2015-04-06 wenzelm 2015-04-06 tuned signature;
2014-11-07 wenzelm 2014-11-07 eliminated pointless check -- command definitions are subject to theory context;
2014-10-14 wenzelm 2014-10-14 tuned signature;
2014-07-04 wenzelm 2014-07-04 insist in explicit overloading;
2014-03-12 wenzelm 2014-03-12 more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges; clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-18 wenzelm 2013-07-18 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;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-26 wenzelm 2012-08-26 entity markup for theory Pure, to enable hyperlinks etc.;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-01 wenzelm 2012-08-01 more standard bootstrapping of Pure.thy;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-03-16 wenzelm 2012-03-16 eliminated odd 'finalconsts' / Theory.add_finals;
2011-11-25 wenzelm 2011-11-25 prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import; prefer non-strict lazy over strict future;
2011-09-07 wenzelm 2011-09-07 explicit join_syntax ensures command transaction integrity of 'theory';
2011-04-20 wenzelm 2011-04-20 added Theory.nodes_of convenience;
2011-04-18 wenzelm 2011-04-18 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);
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 pass plain Proof.context for pretty printing;
2011-04-18 wenzelm 2011-04-18 simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;
2011-04-17 wenzelm 2011-04-17 added Binding.print convenience, which includes quote already;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-20 wenzelm 2011-03-20 tuned;
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-05 wenzelm 2010-09-05 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-27 wenzelm 2010-03-27 disallow premises in primitive Theory.add_def -- handle in Thm.add_def; eliminated obsolete Sign.cert_def; misc tuning and clarification;
2010-03-27 wenzelm 2010-03-27 disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
2010-03-27 wenzelm 2010-03-27 moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML); discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def; modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
2010-03-22 wenzelm 2010-03-22 replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-01-04 wenzelm 2010-01-04 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);
2010-01-04 haftmann 2010-01-04 dropped copy operation for legacy TheoryDataFun
2009-11-15 wenzelm 2009-11-15 primitive defs: clarified def (axiom name) vs. description;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 begin_theory: set theory_name here;
2009-10-25 wenzelm 2009-10-25 make SML/NJ happy;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;