Tue, 16 Jan 2001 00:34:31 +0100 |
wenzelm |
removed Session.finish ();
|
changeset |
files
|
Tue, 16 Jan 2001 00:33:40 +0100 |
wenzelm |
proper induction rule for arbitrarily branching datatype;
|
changeset |
files
|
Tue, 16 Jan 2001 00:32:38 +0100 |
wenzelm |
export inductive_forall_name, inductive_forall_def, rulify;
|
changeset |
files
|
Tue, 16 Jan 2001 00:30:06 +0100 |
wenzelm |
improved string syntax (allow translation rules);
|
changeset |
files
|
Tue, 16 Jan 2001 00:29:43 +0100 |
wenzelm |
renamed Abs_Node_inject to Abs_Node_inj;
|
changeset |
files
|
Tue, 16 Jan 2001 00:29:12 +0100 |
wenzelm |
added atomize_strip_tac;
|
changeset |
files
|
Tue, 16 Jan 2001 00:28:50 +0100 |
wenzelm |
tuned atomize;
|
changeset |
files
|
Tue, 16 Jan 2001 00:27:37 +0100 |
wenzelm |
-f option;
|
changeset |
files
|
Tue, 16 Jan 2001 00:25:54 +0100 |
wenzelm |
removed;
|
changeset |
files
|
Tue, 16 Jan 2001 00:25:25 +0100 |
wenzelm |
removed ex/StringEx.ML;
|
changeset |
files
|
Tue, 16 Jan 2001 00:25:00 +0100 |
wenzelm |
split_conv;
|
changeset |
files
|
Tue, 16 Jan 2001 00:24:36 +0100 |
wenzelm |
updated;
|
changeset |
files
|
Tue, 16 Jan 2001 00:23:14 +0100 |
wenzelm |
isabelle -f;
|
changeset |
files
|
Tue, 16 Jan 2001 00:22:43 +0100 |
wenzelm |
more method_setup examples;
|
changeset |
files
|