src/Pure/Isar/isar_cmd.ML
Sat, 15 Nov 2008 21:31:17 +0100 wenzelm Thm.proof_of returns proof_body;
Sat, 04 Oct 2008 14:29:43 +0200 wenzelm renamed isatool to isabelle_tool in programming interfaces;
Fri, 26 Sep 2008 19:07:56 +0200 wenzelm eliminated polymorphic equality;
Thu, 18 Sep 2008 19:39:44 +0200 wenzelm simplified oracle interface;
Wed, 17 Sep 2008 21:27:38 +0200 wenzelm simplified ML_Context.eval_in -- expect immutable Proof.context value;
Tue, 02 Sep 2008 16:55:33 +0200 wenzelm type Attrib.binding abbreviates Name.binding without attributes;
Tue, 02 Sep 2008 14:10:45 +0200 wenzelm explicit type Name.binding for higher-specification elements;
Thu, 14 Aug 2008 20:13:41 +0200 wenzelm report doc_source;
Thu, 14 Aug 2008 19:52:36 +0200 wenzelm oracle, header/local_theory/proof_markup: pass SymbolPos.text;
Wed, 13 Aug 2008 20:57:26 +0200 wenzelm simplified markup commands -- removed obsolete Present.results, always check text;
Mon, 04 Aug 2008 20:27:40 +0200 wenzelm removed obsolete apply_theorems(_i);
Tue, 29 Jul 2008 08:15:40 +0200 haftmann PureThy: dropped note_thmss_qualified, dropped _i suffix
Tue, 15 Jul 2008 22:37:58 +0200 wenzelm renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
Mon, 14 Jul 2008 19:20:57 +0200 haftmann dropped junk
Mon, 14 Jul 2008 17:51:41 +0200 wenzelm renamed theory to init_theory, removed obsolete kill argument;
Mon, 14 Jul 2008 11:19:39 +0200 wenzelm removed obsolete history commands;
Tue, 08 Jul 2008 17:52:24 +0200 wenzelm moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
Wed, 02 Jul 2008 16:40:17 +0200 wenzelm Toplevel.init_theory: pass name explicitly;
Wed, 25 Jun 2008 17:38:36 +0200 wenzelm moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
Wed, 18 Jun 2008 18:55:06 +0200 wenzelm moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
Sat, 14 Jun 2008 17:26:07 +0200 wenzelm removed exotic 'token_translation' command;
Thu, 17 Apr 2008 16:30:50 +0200 wenzelm token translations: context dependent, result Pretty.T;
Wed, 16 Apr 2008 21:53:02 +0200 wenzelm PureThy.defined_fact;
Tue, 15 Apr 2008 18:49:26 +0200 wenzelm added hide_names command (formerly Sign.hide_names), support fact name space;
Sat, 12 Apr 2008 17:00:35 +0200 wenzelm rep_cterm/rep_thm: no longer dereference theory_ref;
Thu, 10 Apr 2008 13:24:13 +0200 wenzelm Context.set_thread_data: non-critical;
Sat, 29 Mar 2008 22:56:00 +0100 wenzelm simplified print_simpset;
Sat, 29 Mar 2008 19:14:11 +0100 wenzelm removed obsolete use_XXX;
Fri, 28 Mar 2008 20:02:04 +0100 wenzelm Context.>> : operate on Context.generic;
Fri, 28 Mar 2008 00:02:54 +0100 wenzelm reorganized signature of ML_Context;
Thu, 27 Mar 2008 15:32:15 +0100 wenzelm eliminated delayed theory setup
Thu, 27 Mar 2008 14:41:10 +0100 wenzelm renamed ML_Context.the_context to ML_Context.the_global_context;
Wed, 26 Mar 2008 22:40:07 +0100 wenzelm adapted to Context.thread_data interface;
Wed, 26 Mar 2008 20:14:36 +0100 wenzelm removed obsolete use_thy (cf. isar_syn.ML);
Mon, 24 Mar 2008 23:34:24 +0100 wenzelm ML runtime compilation: pass position, tuned signature;
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Thu, 28 Feb 2008 18:59:22 +0100 wenzelm unused_thms: print via official context (ProofContext.pretty_fact),
Thu, 28 Feb 2008 17:33:35 +0100 berghofe Added unused_thms command.
Fri, 15 Feb 2008 14:20:51 +0100 wenzelm tuned names;
Sun, 10 Feb 2008 20:49:47 +0100 wenzelm tuned default position;
Thu, 24 Jan 2008 23:51:17 +0100 wenzelm removed unused Toplevel.properties;
Thu, 03 Jan 2008 22:25:13 +0100 wenzelm nested_command: simplified properties vs. position -- the latter also includes id now;
Wed, 02 Jan 2008 23:00:52 +0100 wenzelm added nested_command (with explicit position argument via properties);
Wed, 07 Nov 2007 22:20:09 +0100 wenzelm Syntax.read_typ;
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Thu, 04 Oct 2007 14:42:47 +0200 wenzelm moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
Mon, 01 Oct 2007 12:25:04 +0200 ballarin Simplified interface for printing of interpretations.
Sat, 08 Sep 2007 19:58:36 +0200 wenzelm thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
Sat, 01 Sep 2007 15:46:59 +0200 wenzelm replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
Fri, 17 Aug 2007 23:10:46 +0200 wenzelm removed obsolete touch_all_thys;
Tue, 07 Aug 2007 20:19:50 +0200 wenzelm theory loader: removed obsolete update_thy (coincides with use_thy);
Wed, 01 Aug 2007 16:55:43 +0200 wenzelm renamed 'print_options' to 'print_configs';
Mon, 30 Jul 2007 11:12:28 +0200 wenzelm marked some CRITICAL sections;
Sat, 28 Jul 2007 22:01:06 +0200 wenzelm type Morphism.declaration;
Sat, 28 Jul 2007 20:40:24 +0200 wenzelm tuned signature;
Fri, 27 Jul 2007 21:55:19 +0200 wenzelm renamed Config to ConfigOption;
Wed, 25 Jul 2007 22:20:51 +0200 wenzelm added command 'print_options';
Mon, 23 Jul 2007 16:45:03 +0200 wenzelm PrintMode.with_modes;
Sun, 22 Jul 2007 13:53:47 +0200 wenzelm simplified ThyInfo.begin_theory;
Thu, 19 Jul 2007 23:18:51 +0200 wenzelm removed obsolete use/update_thy_only;
less more (0) -100 -60 tip