src/Pure/theory.ML
Sun, 13 May 2018 15:05:31 +0200 wenzelm tuned;
Tue, 09 Jan 2018 14:07:39 +0100 wenzelm clarified exception;
Mon, 08 Jan 2018 22:36:02 +0100 wenzelm clarified implicit Pure.thy;
Wed, 19 Apr 2017 12:27:36 +0200 wenzelm proper base name, e.g. relevant for Code_Namespace.hierarchical_program;
Mon, 07 Nov 2016 19:07:30 +0100 wenzelm unused since 15865e0c5598;
Tue, 05 Jul 2016 14:20:27 +0200 wenzelm PIDE reports of implicit variable scope;
Mon, 25 Apr 2016 17:37:36 +0200 wenzelm more rigid check of lhs;
Sun, 24 Apr 2016 20:37:24 +0200 wenzelm within a proof body context, undeclared frees are like global constants;
Mon, 28 Dec 2015 16:29:39 +0100 wenzelm suppress irrelevant position reports;
Fri, 25 Sep 2015 19:13:47 +0200 wenzelm tuned signature: eliminated pointless type Context.pretty;
Thu, 24 Sep 2015 23:33:29 +0200 wenzelm more explicit Defs.context: use proper name spaces as far as possible;
Tue, 22 Sep 2015 22:42:48 +0200 wenzelm tuned signature;
Tue, 22 Sep 2015 22:38:22 +0200 wenzelm eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
Tue, 22 Sep 2015 16:49:56 +0200 wenzelm renamed Defs.node to Defs.item;
Tue, 22 Sep 2015 16:17:49 +0200 wenzelm tuned signature;
Tue, 22 Sep 2015 15:58:19 +0200 wenzelm tuned whitespace;
Tue, 22 Sep 2015 14:32:23 +0200 wenzelm HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
Fri, 28 Aug 2015 23:21:04 +0200 wenzelm more abstract theory certificate, which is not necessarily the full theory;
Sun, 16 Aug 2015 18:19:30 +0200 wenzelm prefer theory_id operations;
Thu, 16 Apr 2015 17:18:48 +0200 wenzelm formal Theory.check, with markup and completion;
Mon, 06 Apr 2015 12:51:25 +0200 wenzelm tuned signature;
Fri, 07 Nov 2014 22:15:51 +0100 wenzelm eliminated pointless check -- command definitions are subject to theory context;
Tue, 14 Oct 2014 10:52:46 +0200 wenzelm tuned signature;
Fri, 04 Jul 2014 17:41:35 +0200 wenzelm insist in explicit overloading;
Wed, 12 Mar 2014 10:42:28 +0100 wenzelm more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
Mon, 10 Mar 2014 13:55:03 +0100 wenzelm abstract type Name_Space.table;
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience;
Tue, 30 Jul 2013 15:09:25 +0200 wenzelm type theory is purely value-oriented;
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;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Sun, 26 Aug 2012 22:23:10 +0200 wenzelm entity markup for theory Pure, to enable hyperlinks etc.;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
Wed, 01 Aug 2012 19:53:20 +0200 wenzelm more standard bootstrapping of Pure.thy;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Fri, 16 Mar 2012 22:48:38 +0100 wenzelm eliminated odd 'finalconsts' / Theory.add_finals;
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;
Wed, 07 Sep 2011 21:05:53 +0200 wenzelm explicit join_syntax ensures command transaction integrity of 'theory';
Wed, 20 Apr 2011 13:54:07 +0200 wenzelm added Theory.nodes_of convenience;
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);
Mon, 18 Apr 2011 14:05:39 +0200 wenzelm pass plain Proof.context for pretty printing;
Mon, 18 Apr 2011 11:44:39 +0200 wenzelm pass plain Proof.context for pretty printing;
Mon, 18 Apr 2011 11:13:29 +0200 wenzelm simplified pretty printing context, which is only required for certain kernel operations;
Sun, 17 Apr 2011 21:42:47 +0200 wenzelm added Binding.print convenience, which includes quote already;
Sun, 17 Apr 2011 19:54:04 +0200 wenzelm report Name_Space.declare/define, relatively to context;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Sun, 20 Mar 2011 22:47:08 +0100 wenzelm tuned;
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
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;
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;
Sat, 27 Mar 2010 17:36:32 +0100 wenzelm disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
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;
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);
Mon, 22 Mar 2010 00:51:18 +0100 wenzelm replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;
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;
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);
Mon, 04 Jan 2010 14:09:56 +0100 haftmann dropped copy operation for legacy TheoryDataFun
Sun, 15 Nov 2009 20:39:22 +0100 wenzelm primitive defs: clarified def (axiom name) vs. description;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Sun, 25 Oct 2009 19:19:29 +0100 wenzelm begin_theory: set theory_name here;
Sun, 25 Oct 2009 13:04:06 +0100 wenzelm make SML/NJ happy;
less more (0) -100 -60 tip