src/Pure/Isar/isar_cmd.ML
Wed, 21 Jul 2010 15:23:46 +0200 wenzelm thm_deps/unused_thms: Context.get_theory based on proper theory ancestry, not accidental theory loader state;
Wed, 21 Jul 2010 13:55:44 +0200 wenzelm thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;
Thu, 03 Jun 2010 22:17:36 +0200 wenzelm diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
Mon, 31 May 2010 21:06:57 +0200 wenzelm modernized some structure names, keeping a few legacy aliases;
Sun, 30 May 2010 21:34:19 +0200 wenzelm replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
Thu, 27 May 2010 18:10:37 +0200 wenzelm renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
Sat, 15 May 2010 23:16:32 +0200 wenzelm refer directly to structure Keyword and Parse;
Sat, 08 May 2010 19:14:13 +0200 wenzelm unified/simplified Pretty.margin_default;
Sun, 25 Apr 2010 21:18:04 +0200 wenzelm replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
Sun, 25 Apr 2010 15:52:03 +0200 wenzelm modernized naming conventions of main Isar proof elements;
Fri, 16 Apr 2010 22:18:59 +0200 wenzelm keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Fri, 16 Apr 2010 20:17:38 +0200 wenzelm modernized old-style type abbreviations;
Mon, 22 Mar 2010 19:23:03 +0100 wenzelm added Specification.axiom convenience;
Sun, 21 Mar 2010 19:28:25 +0100 wenzelm minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
Tue, 16 Feb 2010 11:59:05 +0100 wenzelm simplified meaning of ProofContext.verbose;
Fri, 13 Nov 2009 21:11:15 +0100 wenzelm modernized structure Local_Theory;
Sun, 08 Nov 2009 14:38:36 +0100 wenzelm print_theorems: suppress concealed (global) facts, unless "!" option is given;
Thu, 05 Nov 2009 22:06:46 +0100 wenzelm allow "pervasive" local theory declarations, which are applied the background theory;
Mon, 02 Nov 2009 21:05:47 +0100 wenzelm structure Thm_Deps;
Mon, 02 Nov 2009 20:57:48 +0100 wenzelm modernized structure Proof_Display;
Mon, 02 Nov 2009 20:50:48 +0100 wenzelm modernized structure Proof_Syntax;
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
Wed, 28 Oct 2009 22:02:53 +0100 wenzelm renamed Proof.flat_goal to Proof.simple_goal;
Tue, 27 Oct 2009 13:24:40 +0100 wenzelm ProofContext.setmp_verbose_CRITICAL;
Sat, 24 Oct 2009 19:47:37 +0200 wenzelm renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
Fri, 02 Oct 2009 22:02:11 +0200 wenzelm replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
Tue, 29 Sep 2009 22:15:54 +0200 ballarin Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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.;
Sun, 19 Jul 2009 19:24:04 +0200 wenzelm parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
Sat, 27 Jun 2009 17:35:08 +0200 wenzelm tune File.isabelle_tool signature;
Mon, 30 Mar 2009 22:43:45 +0200 wenzelm tuned;
Mon, 30 Mar 2009 22:38:37 +0200 wenzelm added Toplevel.previous_node_of;
Wed, 18 Mar 2009 22:41:14 +0100 wenzelm more precise type Symbol_Pos.text;
Wed, 18 Mar 2009 21:55:38 +0100 wenzelm de-camelized Symbol_Pos;
Sun, 15 Mar 2009 15:59:43 +0100 wenzelm ML_Syntax.make_binding;
Wed, 11 Mar 2009 23:59:34 +0100 wenzelm added 'local_setup' command;
Sun, 08 Mar 2009 20:31:54 +0100 wenzelm simplified presentation: pass state directly;
Sun, 08 Mar 2009 12:16:12 +0100 wenzelm proper context for Simplifier.pretty_ss;
Sat, 07 Mar 2009 12:07:30 +0100 wenzelm Theory.add_axioms/add_defs: replaced old bstring by binding;
Sat, 07 Mar 2009 11:31:41 +0100 wenzelm oracle: proper name position, tuned;
Thu, 05 Mar 2009 19:48:02 +0100 wenzelm Thm.add_oracle interface: replaced old bstring by binding;
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;
Sat, 28 Feb 2009 18:00:20 +0100 wenzelm moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
Fri, 27 Feb 2009 15:46:22 +0100 wenzelm moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
Fri, 13 Feb 2009 07:53:38 +1100 kleing New command find_consts searching for constants by type (by Timothy Bourke).
Wed, 11 Feb 2009 14:48:14 +1100 kleing FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
Wed, 21 Jan 2009 16:47:04 +0100 haftmann binding replaces bstring
Wed, 07 Jan 2009 16:22:10 +0100 wenzelm qed/after_qed: singleton result;
Mon, 05 Jan 2009 15:55:04 +0100 haftmann locale -> old_locale, new_locale -> locale
Fri, 12 Dec 2008 20:10:22 +0100 ballarin Merged.
Thu, 11 Dec 2008 18:30:26 +0100 ballarin Conversion of HOL-Main and ZF to new locales.
Thu, 11 Dec 2008 17:32:37 +0100 wenzelm print_theorems: more robust difference, even after finished proof;
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
Sun, 16 Nov 2008 20:03:42 +0100 wenzelm clarified Thm.proof_body_of vs. Thm.proof_of;
Sat, 15 Nov 2008 21:31:17 +0100 wenzelm Thm.proof_of returns proof_body;
less more (0) -100 -60 tip