src/Pure/theory.ML
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;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-30 wenzelm 2009-09-30 removed redundant Sign.certify_prop, use Sign.cert_prop instead; tuned;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-07 wenzelm 2009-03-07 Theory.add_axioms/add_defs: replaced old bstring by binding;
2009-03-03 wenzelm 2009-03-03 Binding.str_of;
2009-01-21 wenzelm 2009-01-21 removed Ids;
2009-01-21 haftmann 2009-01-21 binding is alias for Binding.T
2008-12-13 wenzelm 2008-12-13 requires: check ancestors directly;
2008-12-05 haftmann 2008-12-05 removed Table.extend, NameSpace.extend_table
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-03 wenzelm 2008-09-03 simplified specify_const: canonical args, global deps;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-15 wenzelm 2008-04-15 removed obsolete SIGN_THEORY -- no name aliases in structure Theory; removed obsolete BASIC_THEORY;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref; removed obsolete compression;
2007-10-16 wenzelm 2007-10-16 apply_wrappers: perhaps_apply/loop;
2007-10-13 wenzelm 2007-10-13 Theory.specify_const: added deps argument;
2007-10-11 wenzelm 2007-10-11 dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 wenzelm 2007-10-11 added specify_const;
2007-09-29 wenzelm 2007-09-29 Sign.the_const_constraint;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read; no export of read/cert_axm;
2007-09-20 wenzelm 2007-09-20 tuned signature; moved generic interpretation to interpretation.ML; added abstract at_begin/end wrappers;
2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-08-09 haftmann 2007-08-09 new access interface in defs.ML
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;