src/Pure/theory.ML
2 months ago ago clarified signature;
6 months ago ago clarified signature;
11 months ago ago clarified document antiquotation @{theory};
11 months ago ago clarified signature;
12 months ago ago tuned;
16 months ago ago clarified exception;
16 months ago ago clarified implicit Pure.thy;
2017-04-19 ago proper base name, e.g. relevant for Code_Namespace.hierarchical_program;
2016-11-07 ago unused since 15865e0c5598;
2016-07-05 ago PIDE reports of implicit variable scope;
2016-04-25 ago more rigid check of lhs;
2016-04-24 ago within a proof body context, undeclared frees are like global constants;
2015-12-28 ago suppress irrelevant position reports;
2015-09-25 ago tuned signature: eliminated pointless type Context.pretty;
2015-09-24 ago more explicit Defs.context: use proper name spaces as far as possible;
2015-09-22 ago tuned signature;
2015-09-22 ago eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
2015-09-22 ago renamed Defs.node to Defs.item;
2015-09-22 ago tuned signature;
2015-09-22 ago tuned whitespace;
2015-09-22 ago HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
2015-08-28 ago more abstract theory certificate, which is not necessarily the full theory;
2015-08-16 ago prefer theory_id operations;
2015-04-16 ago formal Theory.check, with markup and completion;
2015-04-06 ago tuned signature;
2014-11-07 ago eliminated pointless check -- command definitions are subject to theory context;
2014-10-14 ago tuned signature;
2014-07-04 ago insist in explicit overloading;
2014-03-12 ago more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
2014-03-10 ago abstract type Name_Space.table;
2013-08-23 ago added Theory.setup convenience;
2013-07-30 ago type theory is purely value-oriented;
2013-07-18 ago 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 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-08-26 ago entity markup for theory Pure, to enable hyperlinks etc.;
2012-08-26 ago theory def/ref position reports, which enable hyperlinks etc.;
2012-08-01 ago more standard bootstrapping of Pure.thy;
2012-03-18 ago maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
2012-03-16 ago eliminated odd 'finalconsts' / Theory.add_finals;
2011-11-25 ago prefer Parser.make_gram over Parser.merge_gram, to approximate n-ary merges on theory import;
2011-09-07 ago explicit join_syntax ensures command transaction integrity of 'theory';
2011-04-20 ago added Theory.nodes_of convenience;
2011-04-18 ago 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 ago pass plain Proof.context for pretty printing;
2011-04-18 ago pass plain Proof.context for pretty printing;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-17 ago added Binding.print convenience, which includes quote already;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-03-20 ago tuned;
2010-09-05 ago turned show_sorts/show_types into proper configuration options;
2010-09-05 ago pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-27 ago disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
2010-03-27 ago disallow sort constraints in primitive Theory.add_axiom/add_def -- handled in Thm.add_axiom/add_def;
2010-03-27 ago moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
2010-03-22 ago replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-01-04 ago 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 ago dropped copy operation for legacy TheoryDataFun