src/Pure/Isar/obtain.ML
Tue, 28 Feb 2012 16:43:32 +0100 wenzelm display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
Sat, 14 Jan 2012 21:16:15 +0100 wenzelm discontinued old-style Term.list_abs in favour of plain Term.abs;
Sat, 14 Jan 2012 17:45:04 +0100 wenzelm discontinued old-style Term.list_all_free in favour of plain Logic.all;
Mon, 07 Nov 2011 17:00:23 +0100 wenzelm tuned signature -- avoid spurious Thm.mixed_attribute;
Thu, 03 Nov 2011 23:55:53 +0100 wenzelm more general Proof_Context.bind_propp, which allows outer parameters;
Thu, 03 Nov 2011 22:51:37 +0100 wenzelm tuned signature;
Thu, 03 Nov 2011 22:23:41 +0100 wenzelm tuned signature -- canonical argument order;
Thu, 09 Jun 2011 16:34:49 +0200 wenzelm discontinued Name.variant to emphasize that this is old-style / indirect;
Thu, 28 Apr 2011 20:20:49 +0200 wenzelm eliminated slightly odd Proof_Context.bind_fixes;
Wed, 27 Apr 2011 23:02:43 +0200 wenzelm more precise positions via binding;
Wed, 27 Apr 2011 21:50:04 +0200 wenzelm clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
Wed, 27 Apr 2011 20:58:40 +0200 wenzelm tuned signature -- eliminated odd comment;
Wed, 27 Apr 2011 19:55:42 +0200 wenzelm more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;
Wed, 27 Apr 2011 17:58:45 +0200 wenzelm reorganized fixes as specialized (global) name space;
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;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
Sun, 05 Sep 2010 21:41:24 +0200 wenzelm turned show_sorts/show_types into proper configuration options;
Mon, 30 Aug 2010 15:19:39 +0200 wenzelm tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
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;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Wed, 25 Nov 2009 09:13:46 +0100 haftmann normalized uncurry take/drop
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
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;
Sat, 17 Oct 2009 15:57:51 +0200 wenzelm indicate CRITICAL nature of various setmp combinators;
Wed, 30 Sep 2009 22:25:50 +0200 wenzelm eliminated dead code;
Sun, 26 Jul 2009 13:12:54 +0200 wenzelm Variable.focus: named parameters;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Wed, 24 Jun 2009 21:28:02 +0200 wenzelm renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
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 16:31:16 +0100 wenzelm replaced add_binds(_i) by bind_terms -- internal version only;
Thu, 19 Mar 2009 13:28:55 +0100 wenzelm use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
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;
Tue, 03 Mar 2009 14:07:43 +0100 wenzelm Thm.binding;
Wed, 21 Jan 2009 16:47:32 +0100 haftmann binding is alias for Binding.T
Wed, 07 Jan 2009 16:22:10 +0100 wenzelm qed/after_qed: singleton result;
Fri, 05 Dec 2008 18:43:42 +0100 haftmann Name.name_of -> Binding.base_name
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Tue, 02 Sep 2008 16:55:33 +0200 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
Tue, 02 Sep 2008 14:10:30 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Tue, 03 Apr 2007 19:24:13 +0200 wenzelm renamed Variable.import to import_thms (avoid clash with Alice keywords);
Wed, 06 Dec 2006 21:19:03 +0100 wenzelm export: added explicit term operation;
Thu, 30 Nov 2006 14:17:29 +0100 wenzelm qualified MetaSimplifier.norm_hhf(_protect);
Tue, 07 Nov 2006 19:39:50 +0100 wenzelm moved statement to specification.ML;
Sat, 30 Sep 2006 21:39:31 +0200 wenzelm statement: Variable.fix_frees;
Wed, 02 Aug 2006 22:27:02 +0200 wenzelm added tactical result;
Thu, 27 Jul 2006 13:43:01 +0200 wenzelm moved basic assumption operations from structure ProofContext to Assumption;
Wed, 26 Jul 2006 19:37:41 +0200 wenzelm Variable.import(T): result includes fixed types/terms;
Tue, 25 Jul 2006 21:18:08 +0200 wenzelm added find_free (from term.ML);
Tue, 11 Jul 2006 12:17:11 +0200 wenzelm replaced Term.variant(list) by Name.variant(_list);
Tue, 04 Jul 2006 19:49:55 +0200 wenzelm guess: proper context for polymorphic parameters;
Mon, 03 Jul 2006 19:33:09 +0200 wenzelm obtain_export: Thm.generalize;
less more (0) -100 -60 tip