| Wed, 04 Mar 2009 11:48:52 +0100 |
nipkow |
Option.thy
|
changeset |
files
|
| Wed, 04 Mar 2009 11:44:05 +0100 |
haftmann |
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
|
changeset |
files
|
| Wed, 04 Mar 2009 11:37:50 +0100 |
haftmann |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 10:52:47 +0100 |
haftmann |
explicit error message for `improper` instances lacking explicit instance parameter constants
|
changeset |
files
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
changeset |
files
|
| Wed, 04 Mar 2009 11:05:02 +0100 |
blanchet |
Merge.
|
changeset |
files
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
changeset |
files
|
| Wed, 04 Mar 2009 10:43:39 +0100 |
blanchet |
Made Refute.norm_rhs public, so I can use it in Nitpick.
|
changeset |
files
|
| Sun, 01 Mar 2009 18:40:16 +0100 |
blanchet |
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
|
changeset |
files
|
| Tue, 24 Feb 2009 16:12:27 +0100 |
blanchet |
Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
|
changeset |
files
|
| Wed, 04 Mar 2009 10:47:35 +0100 |
nipkow |
merged
|
changeset |
files
|
| Wed, 04 Mar 2009 10:47:20 +0100 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
changeset |
files
|
| 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);
|
changeset |
files
|
| Tue, 03 Mar 2009 21:53:52 +0100 |
wenzelm |
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
|
changeset |
files
|
| Tue, 03 Mar 2009 21:49:34 +0100 |
wenzelm |
tuned str_of, now subject to verbose flag;
|
changeset |
files
|
| Tue, 03 Mar 2009 21:49:05 +0100 |
wenzelm |
added @{binding} ML antiquotations;
|
changeset |
files
|
| Tue, 03 Mar 2009 21:48:40 +0100 |
wenzelm |
added print_properties, print_position (again);
|
changeset |
files
|
| Tue, 03 Mar 2009 19:30:43 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 03 Mar 2009 19:21:10 +0100 |
haftmann |
merged
|
changeset |
files
|
| Tue, 03 Mar 2009 13:20:53 +0100 |
haftmann |
tuned manuals
|
changeset |
files
|
| Tue, 03 Mar 2009 11:00:51 +0100 |
haftmann |
more canonical directory structure of manuals
|
changeset |
files
|
| Tue, 03 Mar 2009 18:33:21 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 03 Mar 2009 17:05:18 +0100 |
nipkow |
removed and renamed redundant lemmas
|
changeset |
files
|
| 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;
|
changeset |
files
|
| Tue, 03 Mar 2009 18:31:59 +0100 |
wenzelm |
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
|
changeset |
files
|
| Tue, 03 Mar 2009 17:42:30 +0100 |
wenzelm |
added markup for binding;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:12:52 +0100 |
wenzelm |
Binding.str_of;
|
changeset |
files
|
| Tue, 03 Mar 2009 15:09:09 +0100 |
wenzelm |
Binding.str_of;
|
changeset |
files
|