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;
|
file |
diff |
annotate
|
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);
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Fri, 13 Feb 2009 07:53:38 +1100 |
kleing |
New command find_consts searching for constants by type (by Timothy Bourke).
|
file |
diff |
annotate
|
Wed, 11 Feb 2009 14:48:14 +1100 |
kleing |
FindTheorems: add solves feature; tidy up const name subsettin; patch by Timothy Bourke
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
Wed, 07 Jan 2009 16:22:10 +0100 |
wenzelm |
qed/after_qed: singleton result;
|
file |
diff |
annotate
|
Mon, 05 Jan 2009 15:55:04 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
file |
diff |
annotate
|
Fri, 12 Dec 2008 20:10:22 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
Thu, 11 Dec 2008 17:32:37 +0100 |
wenzelm |
print_theorems: more robust difference, even after finished proof;
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 18:43:42 +0100 |
haftmann |
Name.name_of -> Binding.base_name
|
file |
diff |
annotate
|
Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
Sun, 16 Nov 2008 20:03:42 +0100 |
wenzelm |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
file |
diff |
annotate
|
Sat, 15 Nov 2008 21:31:17 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
file |
diff |
annotate
|
Sat, 04 Oct 2008 14:29:43 +0200 |
wenzelm |
renamed isatool to isabelle_tool in programming interfaces;
|
file |
diff |
annotate
|
Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
Wed, 17 Sep 2008 21:27:38 +0200 |
wenzelm |
simplified ML_Context.eval_in -- expect immutable Proof.context value;
|
file |
diff |
annotate
|
Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
Thu, 14 Aug 2008 20:13:41 +0200 |
wenzelm |
report doc_source;
|
file |
diff |
annotate
|
Thu, 14 Aug 2008 19:52:36 +0200 |
wenzelm |
oracle, header/local_theory/proof_markup: pass SymbolPos.text;
|
file |
diff |
annotate
|
Wed, 13 Aug 2008 20:57:26 +0200 |
wenzelm |
simplified markup commands -- removed obsolete Present.results, always check text;
|
file |
diff |
annotate
|
Mon, 04 Aug 2008 20:27:40 +0200 |
wenzelm |
removed obsolete apply_theorems(_i);
|
file |
diff |
annotate
|
Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
Tue, 15 Jul 2008 22:37:58 +0200 |
wenzelm |
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 19:20:57 +0200 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 17:51:41 +0200 |
wenzelm |
renamed theory to init_theory, removed obsolete kill argument;
|
file |
diff |
annotate
|
Mon, 14 Jul 2008 11:19:39 +0200 |
wenzelm |
removed obsolete history commands;
|
file |
diff |
annotate
|
Tue, 08 Jul 2008 17:52:24 +0200 |
wenzelm |
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
|
file |
diff |
annotate
|
Wed, 02 Jul 2008 16:40:17 +0200 |
wenzelm |
Toplevel.init_theory: pass name explicitly;
|
file |
diff |
annotate
|
Wed, 25 Jun 2008 17:38:36 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
Wed, 18 Jun 2008 18:55:06 +0200 |
wenzelm |
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
|
file |
diff |
annotate
|
Sat, 14 Jun 2008 17:26:07 +0200 |
wenzelm |
removed exotic 'token_translation' command;
|
file |
diff |
annotate
|
Thu, 17 Apr 2008 16:30:50 +0200 |
wenzelm |
token translations: context dependent, result Pretty.T;
|
file |
diff |
annotate
|
Wed, 16 Apr 2008 21:53:02 +0200 |
wenzelm |
PureThy.defined_fact;
|
file |
diff |
annotate
|
Tue, 15 Apr 2008 18:49:26 +0200 |
wenzelm |
added hide_names command (formerly Sign.hide_names), support fact name space;
|
file |
diff |
annotate
|
Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
Thu, 10 Apr 2008 13:24:13 +0200 |
wenzelm |
Context.set_thread_data: non-critical;
|
file |
diff |
annotate
|
Sat, 29 Mar 2008 22:56:00 +0100 |
wenzelm |
simplified print_simpset;
|
file |
diff |
annotate
|
Sat, 29 Mar 2008 19:14:11 +0100 |
wenzelm |
removed obsolete use_XXX;
|
file |
diff |
annotate
|
Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
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
|