| Thu, 29 Oct 2009 11:56:02 +0100 |
wenzelm |
less hermetic ML;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 22:02:53 +0100 |
wenzelm |
renamed Proof.flat_goal to Proof.simple_goal;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 16:41:22 +1100 |
kleing |
find_theorems: better handling of abbreviations (by Timothy Bourke)
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 00:32:00 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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.;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 17:07:26 +0200 |
wenzelm |
more detailed start_timing/end_timing;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 15:14:48 +0200 |
wenzelm |
minor tuning according to Isabelle/ML conventions;
|
file |
diff |
annotate
|
| Wed, 06 May 2009 10:55:47 +1000 |
Timothy Bourke |
Prototype introiff option for find_theorems.
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 20:40:25 +0200 |
wenzelm |
superficial tuning;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2009 12:25:52 +1100 |
Timothy Bourke |
Limit the number of results returned by auto_solves.
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 15:55:11 +1100 |
Timothy Bourke |
Use assms rather than prems in find_theorems solves.
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 15:54:58 +0100 |
wenzelm |
Assumption.all_prems_of, Assumption.all_assms_of;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 22:32:27 +0100 |
wenzelm |
replaced archaic use of rep_ss by Simplifier.mksimps;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 00:05:20 +0100 |
wenzelm |
renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:54:12 +0100 |
wenzelm |
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 16:22:37 +0100 |
wenzelm |
avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 14:45:23 +0100 |
wenzelm |
replaced archaic Display.pretty_fact by FindTheorems.pretty_thm, which observes the context properly (as did the former prt_fact already);
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 16:05:40 +0100 |
wenzelm |
observe basic Isabelle/ML coding conventions;
|
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
| base
|