src/Pure/Isar/isar_cmd.ML
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;
Mon, 09 Jul 2007 11:44:20 +0200 wenzelm type output = string indicates raw system output;
Tue, 26 Jun 2007 00:35:14 +0200 wenzelm fixed undo: try undos_proof first!
Tue, 08 May 2007 17:40:20 +0200 wenzelm tuned ProofDisplay.pretty_full_theory;
Thu, 05 Apr 2007 00:30:32 +0200 wenzelm thy_deps: sort Context.thy_ord;
Wed, 04 Apr 2007 23:29:42 +0200 wenzelm simplified thy_deps using Theory.ancestors_of (in order of creation);
Tue, 03 Apr 2007 19:24:19 +0200 wenzelm avoid clash with Alice keywords;
Tue, 20 Mar 2007 15:52:42 +0100 haftmann added theory dependency graph
Tue, 20 Feb 2007 00:14:33 +0100 kleing Remove duplicates from printed theorems in find_theorems
Sun, 04 Feb 2007 22:02:19 +0100 wenzelm tuned oracle interface;
Sun, 28 Jan 2007 23:29:16 +0100 wenzelm added simproc_setup;
Fri, 19 Jan 2007 22:08:25 +0100 wenzelm added various ML setup functions (from sign.ML, pure_thy.ML);
Fri, 19 Jan 2007 13:09:35 +0100 wenzelm added 'declaration' command;
Sat, 30 Dec 2006 12:33:25 +0100 wenzelm removed obsolete clear_undos_theory;
Fri, 29 Dec 2006 19:50:48 +0100 wenzelm removed obsolete init_context;
Fri, 15 Dec 2006 00:08:06 +0100 wenzelm avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
Sat, 09 Dec 2006 18:05:44 +0100 wenzelm added print_abbrevs;
Tue, 05 Dec 2006 22:14:48 +0100 wenzelm print_syntax etc.: plain Toplevel.context_of;
Tue, 28 Nov 2006 00:35:21 +0100 wenzelm dest_term: strip_imp_concl;
Thu, 23 Nov 2006 22:38:30 +0100 wenzelm prefer Proof.context over Context.generic;
Tue, 21 Nov 2006 18:07:33 +0100 wenzelm moved theorem kinds from PureThy to Thm;
Tue, 14 Nov 2006 00:15:38 +0100 wenzelm incorporated IsarThy into IsarCmd;
Thu, 12 Oct 2006 22:57:32 +0200 wenzelm renamed print_lthms to print_facts, do not insist on proof state;
Wed, 11 Oct 2006 22:55:15 +0200 wenzelm removed 'undo_end', recovered 'cannot_undo';
Wed, 11 Oct 2006 00:27:30 +0200 wenzelm undo_end/kill: handle local theory;
Mon, 09 Oct 2006 19:37:06 +0200 wenzelm Secure.commit;
Sat, 30 Sep 2006 21:39:29 +0200 wenzelm added undo_end;
Tue, 19 Sep 2006 23:15:26 +0200 wenzelm 'print_theory': bang option for full verbosity;
Mon, 18 Sep 2006 19:12:46 +0200 wenzelm added class_deps;
Thu, 13 Apr 2006 12:01:08 +0200 wenzelm ProofDisplay.print_theorems/theory;
Sun, 09 Apr 2006 18:51:20 +0200 wenzelm print_term etc.: actually observe print mode in final output;
Tue, 14 Mar 2006 22:06:37 +0100 wenzelm added print_stmts;
Wed, 15 Feb 2006 21:35:07 +0100 wenzelm simplified presentation commands;
Fri, 27 Jan 2006 19:03:09 +0100 wenzelm Locale.init;
Tue, 10 Jan 2006 19:33:38 +0100 wenzelm print rules: generic context;
Thu, 05 Jan 2006 22:29:59 +0100 wenzelm tuned print_theorems_theory;
Wed, 09 Nov 2005 16:26:50 +0100 wenzelm Element.context;
Wed, 02 Nov 2005 14:47:00 +0100 wenzelm Isar.loop;
Tue, 18 Oct 2005 17:59:32 +0200 wenzelm back: Toplevel.actual/skip_proof;
Tue, 13 Sep 2005 22:19:36 +0200 wenzelm Proof.get_thmss;
Mon, 05 Sep 2005 17:38:20 +0200 wenzelm add_chapter/section/subsection/subsubsection/text: optional locale specification;
less more (0) -100 -60 tip