src/Pure/Isar/specification.ML
Sat, 19 Nov 2011 13:02:50 +0100 wenzelm do not store vacuous theorem specifications -- relevant for frugal local theory content;
Sat, 19 Nov 2011 12:33:18 +0100 wenzelm put structural attributes of 'obtains' in outer declarations, to make it actually work in local theory;
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute;
Thu, 03 Nov 2011 22:23:41 +0100 wenzelm tuned signature -- canonical argument order;
Sat, 13 Aug 2011 22:04:07 +0200 wenzelm less verbosity in batch mode -- spam reduction and notable performance improvement;
Thu, 09 Jun 2011 20:22:22 +0200 wenzelm tuned signature: Name.invent and Name.invent_names;
Wed, 27 Apr 2011 20:58:40 +0200 wenzelm tuned signature -- eliminated odd comment;
Wed, 27 Apr 2011 10:31:18 +0200 wenzelm more uniform Variable.add_frees/add_fixed etc.;
Thu, 21 Apr 2011 12:56:27 +0200 wenzelm discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
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;
Sat, 16 Apr 2011 12:46:18 +0200 wenzelm tuned signature, disentangled dependencies;
Wed, 06 Apr 2011 23:17:45 +0200 wenzelm parallel parsing of big specifications;
Thu, 24 Mar 2011 16:56:19 +0100 wenzelm added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
Sat, 08 Jan 2011 17:14:48 +0100 wenzelm misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
Mon, 20 Sep 2010 16:05:25 +0200 wenzelm renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Thu, 12 Aug 2010 13:23:46 +0200 haftmann Named_Target.theory_init
Wed, 11 Aug 2010 14:45:38 +0200 haftmann renamed Theory_Target to the more appropriate Named_Target
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Thu, 27 May 2010 17:41:27 +0200 wenzelm renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
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;
Thu, 29 Apr 2010 16:55:22 +0200 wenzelm ProofContext.read_const: allow for type constraint (for fixed variable);
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Fri, 23 Apr 2010 22:48:07 +0200 wenzelm explicit 'schematic_theorem' etc. for schematic theorem statements;
Sun, 11 Apr 2010 14:30:34 +0200 wenzelm Thm.add_axiom/add_def: return internal name of foundational axiom;
Mon, 22 Mar 2010 19:23:03 +0100 wenzelm added Specification.axiom convenience;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Sun, 07 Mar 2010 11:57:16 +0100 wenzelm modernized structure Local_Defs;
Mon, 01 Mar 2010 17:09:42 +0100 wenzelm added type_notation command;
Sat, 27 Feb 2010 20:51:51 +0100 wenzelm clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
Thu, 19 Nov 2009 14:45:56 +0100 wenzelm Specification.definition: Thm.definitionK marks exactly the high-level end-user result;
Thu, 19 Nov 2009 08:25:57 +0100 bulwahn replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
Sun, 15 Nov 2009 20:57:42 +0100 wenzelm axiomatization: declare Spec_Rules, direct result;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Fri, 13 Nov 2009 20:41:29 +0100 wenzelm eliminated slightly odd kind argument of LocalTheory.note(s);
Thu, 12 Nov 2009 22:29:54 +0100 wenzelm eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Thu, 05 Nov 2009 20:44:42 +0100 wenzelm declare Spec_Rules for most basic definitional packages;
Mon, 02 Nov 2009 20:57:48 +0100 wenzelm modernized structure Proof_Display;
Mon, 02 Nov 2009 20:45:23 +0100 wenzelm modernized structure AutoBind;
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
Sun, 01 Nov 2009 15:24:45 +0100 wenzelm modernized structure Rule_Cases;
Sun, 25 Oct 2009 21:35:46 +0100 wenzelm eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
Fri, 02 Oct 2009 21:39:06 +0200 wenzelm clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
Wed, 30 Sep 2009 22:25:50 +0200 wenzelm eliminated dead code;
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn handling of definitions
Wed, 23 Sep 2009 16:20:12 +0200 bulwahn experimenting to add some useful interface for definitions
Sat, 28 Mar 2009 17:53:33 +0100 wenzelm renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
Sat, 28 Mar 2009 17:21:11 +0100 wenzelm renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;
Thu, 19 Mar 2009 13:28:55 +0100 wenzelm use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
Thu, 12 Mar 2009 21:37:18 +0100 wenzelm simplified versions check_spec, read_spec, check_free_spec, read_free_spec: operate on list of singleton statements;
Thu, 12 Mar 2009 15:54:19 +0100 wenzelm Assumption.local_prems_of;
Thu, 12 Mar 2009 14:30:23 +0100 wenzelm axiomatization: more precise treatment of binding;
Wed, 11 Mar 2009 15:38:25 +0100 wenzelm Thm.def_binding_optional;
Sat, 07 Mar 2009 22:16:50 +0100 wenzelm more uniform handling of binding in targets and derived elements;
Tue, 03 Mar 2009 18:32:01 +0100 wenzelm renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Fri, 19 Dec 2008 16:39:23 +0100 ballarin All logics ported to new locales.
less more (0) -100 -60 tip