| Fri, 28 Mar 2008 00:02:54 +0100 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:10 +0100 |
wenzelm |
renamed ML_Context.the_context to ML_Context.the_global_context;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:07 +0100 |
wenzelm |
adapted to Context.thread_data interface;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 20:14:36 +0100 |
wenzelm |
removed obsolete use_thy (cf. isar_syn.ML);
|
file |
diff |
annotate
|
| Mon, 24 Mar 2008 23:34:24 +0100 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2008 18:59:22 +0100 |
wenzelm |
unused_thms: print via official context (ProofContext.pretty_fact),
|
file |
diff |
annotate
|
| Thu, 28 Feb 2008 17:33:35 +0100 |
berghofe |
Added unused_thms command.
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 14:20:51 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Sun, 10 Feb 2008 20:49:47 +0100 |
wenzelm |
tuned default position;
|
file |
diff |
annotate
|
| Thu, 24 Jan 2008 23:51:17 +0100 |
wenzelm |
removed unused Toplevel.properties;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 22:25:13 +0100 |
wenzelm |
nested_command: simplified properties vs. position -- the latter also includes id now;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 23:00:52 +0100 |
wenzelm |
added nested_command (with explicit position argument via properties);
|
file |
diff |
annotate
|
| Wed, 07 Nov 2007 22:20:09 +0100 |
wenzelm |
Syntax.read_typ;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2007 12:25:04 +0200 |
ballarin |
Simplified interface for printing of interpretations.
|
file |
diff |
annotate
|
| Sat, 08 Sep 2007 19:58:36 +0200 |
wenzelm |
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 15:46:59 +0200 |
wenzelm |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 23:10:46 +0200 |
wenzelm |
removed obsolete touch_all_thys;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 20:19:50 +0200 |
wenzelm |
theory loader: removed obsolete update_thy (coincides with use_thy);
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 16:55:43 +0200 |
wenzelm |
renamed 'print_options' to 'print_configs';
|
file |
diff |
annotate
|
| Mon, 30 Jul 2007 11:12:28 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 22:01:06 +0200 |
wenzelm |
type Morphism.declaration;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2007 21:55:19 +0200 |
wenzelm |
renamed Config to ConfigOption;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 22:20:51 +0200 |
wenzelm |
added command 'print_options';
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 16:45:03 +0200 |
wenzelm |
PrintMode.with_modes;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 13:53:47 +0200 |
wenzelm |
simplified ThyInfo.begin_theory;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 23:18:51 +0200 |
wenzelm |
removed obsolete use/update_thy_only;
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 11:44:20 +0200 |
wenzelm |
type output = string indicates raw system output;
|
file |
diff |
annotate
|
| Tue, 26 Jun 2007 00:35:14 +0200 |
wenzelm |
fixed undo: try undos_proof first!
|
file |
diff |
annotate
|
| Tue, 08 May 2007 17:40:20 +0200 |
wenzelm |
tuned ProofDisplay.pretty_full_theory;
|
file |
diff |
annotate
|
| Thu, 05 Apr 2007 00:30:32 +0200 |
wenzelm |
thy_deps: sort Context.thy_ord;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:42 +0200 |
wenzelm |
simplified thy_deps using Theory.ancestors_of (in order of creation);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:19 +0200 |
wenzelm |
avoid clash with Alice keywords;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:42 +0100 |
haftmann |
added theory dependency graph
|
file |
diff |
annotate
|
| Tue, 20 Feb 2007 00:14:33 +0100 |
kleing |
Remove duplicates from printed theorems in find_theorems
|
file |
diff |
annotate
|
| Sun, 04 Feb 2007 22:02:19 +0100 |
wenzelm |
tuned oracle interface;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2007 23:29:16 +0100 |
wenzelm |
added simproc_setup;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:25 +0100 |
wenzelm |
added various ML setup functions (from sign.ML, pure_thy.ML);
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 13:09:35 +0100 |
wenzelm |
added 'declaration' command;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 12:33:25 +0100 |
wenzelm |
removed obsolete clear_undos_theory;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2006 19:50:48 +0100 |
wenzelm |
removed obsolete init_context;
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:44 +0100 |
wenzelm |
added print_abbrevs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:48 +0100 |
wenzelm |
print_syntax etc.: plain Toplevel.context_of;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:21 +0100 |
wenzelm |
dest_term: strip_imp_concl;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 22:38:30 +0100 |
wenzelm |
prefer Proof.context over Context.generic;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:33 +0100 |
wenzelm |
moved theorem kinds from PureThy to Thm;
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 00:15:38 +0100 |
wenzelm |
incorporated IsarThy into IsarCmd;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2006 22:57:32 +0200 |
wenzelm |
renamed print_lthms to print_facts, do not insist on proof state;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 22:55:15 +0200 |
wenzelm |
removed 'undo_end', recovered 'cannot_undo';
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 00:27:30 +0200 |
wenzelm |
undo_end/kill: handle local theory;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 19:37:06 +0200 |
wenzelm |
Secure.commit;
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 21:39:29 +0200 |
wenzelm |
added undo_end;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:26 +0200 |
wenzelm |
'print_theory': bang option for full verbosity;
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:12:46 +0200 |
wenzelm |
added class_deps;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:08 +0200 |
wenzelm |
ProofDisplay.print_theorems/theory;
|
file |
diff |
annotate
|