| Wed, 11 Mar 2009 23:59:34 +0100 |
wenzelm |
added 'local_setup' command;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 11:31:41 +0100 |
wenzelm |
oracle: proper name position, tuned;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 16:48:06 +0100 |
wenzelm |
discontinued experimental support for Alice -- too hard to maintain its many language incompatibilities, never really worked anyway;
|
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 23:40:23 +0100 |
haftmann |
allow empty class specs
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:03 +0100 |
haftmann |
wrecked old locale package and related modules
|
file |
diff |
annotate
|
| Wed, 07 Jan 2009 22:31:34 +0100 |
haftmann |
changed locale predicate name convention
|
file |
diff |
annotate
|
| Wed, 07 Jan 2009 08:03:25 +0100 |
haftmann |
proper local_theory after Class.class
|
file |
diff |
annotate
|
| Tue, 06 Jan 2009 08:50:12 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 15:55:04 +0100 |
haftmann |
locale -> old_locale, new_locale -> locale
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 15:36:24 +0100 |
haftmann |
rearranged target theories
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 00:13:11 +0100 |
wenzelm |
Isar.init;
|
file |
diff |
annotate
|
| Fri, 02 Jan 2009 15:44:32 +0100 |
wenzelm |
added props_text (from outer_parse.ML);
|
file |
diff |
annotate
|
| Fri, 12 Dec 2008 14:23:49 +0100 |
ballarin |
Merged; updated interpretation command in isar_syn.ML.
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 10:11:18 +0100 |
ballarin |
Enable keyword 'structure' in for clause of locale expression.
|
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
|
| Wed, 03 Dec 2008 15:27:41 +0100 |
ballarin |
Sublocale: removed public after_qed; identifiers private to NewLocale.
|
file |
diff |
annotate
|
| Fri, 28 Nov 2008 12:26:14 +0100 |
ballarin |
Ahere to modern naming conventions; proper treatment of internal vs external names.
|
file |
diff |
annotate
|
| Thu, 27 Nov 2008 10:29:07 +0100 |
ballarin |
Sublocale command.
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:22 +0100 |
haftmann |
adjusted locale signature to *_cmd convention
|
file |
diff |
annotate
|
| Thu, 06 Nov 2008 12:29:51 +0100 |
ballarin |
Keyword 'includes' gone.
|
file |
diff |
annotate
|
| Fri, 19 Sep 2008 21:00:48 +0200 |
wenzelm |
moved Isar editor commands from isar_syn.ML to isar.ML;
|
file |
diff |
annotate
|