| Sat, 29 May 2004 15:08:08 +0200 |
wenzelm |
handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
|
changeset |
files
|
| Sat, 29 May 2004 15:07:42 +0200 |
wenzelm |
tuned _dummy_ofsort syntax;
|
changeset |
files
|
| Sat, 29 May 2004 15:07:29 +0200 |
wenzelm |
added pp_show_brackets; support unbreakable blocks;
|
changeset |
files
|
| Sat, 29 May 2004 15:07:05 +0200 |
wenzelm |
transform_error;
|
changeset |
files
|
| Sat, 29 May 2004 15:06:42 +0200 |
wenzelm |
Library.read_int; Output.output;
|
changeset |
files
|
| Sat, 29 May 2004 15:06:19 +0200 |
wenzelm |
improved support for raw symbols;
|
changeset |
files
|
| Sat, 29 May 2004 15:06:04 +0200 |
wenzelm |
Output.error;
|
changeset |
files
|
| Sat, 29 May 2004 15:05:51 +0200 |
wenzelm |
pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
|
changeset |
files
|
| Sat, 29 May 2004 15:05:37 +0200 |
wenzelm |
added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
|
changeset |
files
|
| Sat, 29 May 2004 15:05:25 +0200 |
wenzelm |
removed norm_typ; improved output; refer to Pretty.pp;
|
changeset |
files
|
| Sat, 29 May 2004 15:05:02 +0200 |
wenzelm |
moved read_int etc. to library.ML; added type 'arity';
|
changeset |
files
|
| Sat, 29 May 2004 15:03:59 +0200 |
wenzelm |
improved output; refer to Pretty.pp;
|
changeset |
files
|
| Sat, 29 May 2004 15:02:35 +0200 |
wenzelm |
Output.add_mode; Output.timing;
|
changeset |
files
|
| Sat, 29 May 2004 15:02:13 +0200 |
wenzelm |
output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
|
changeset |
files
|
| Sat, 29 May 2004 15:01:36 +0200 |
wenzelm |
Output.timing;
|
changeset |
files
|
| Sat, 29 May 2004 15:00:52 +0200 |
wenzelm |
improved output;
|
changeset |
files
|
| Sat, 29 May 2004 15:00:25 +0200 |
wenzelm |
moved print_mode to General/output.ML; load General/pretty.ML early;
|
changeset |
files
|
| Sat, 29 May 2004 15:00:14 +0200 |
wenzelm |
added Pure/General/output.ML;
|
changeset |
files
|
| Sat, 29 May 2004 14:59:57 +0200 |
wenzelm |
avoid 'handle _' -- would cover Interrupt as well!!!
|
changeset |
files
|
| Sat, 29 May 2004 14:59:24 +0200 |
wenzelm |
Sign.infer_types: Sign.pp;
|
changeset |
files
|
| Sat, 29 May 2004 14:58:44 +0200 |
wenzelm |
Library.read_int;
|
changeset |
files
|
| Sat, 29 May 2004 14:57:39 +0200 |
wenzelm |
Output.output;
|
changeset |
files
|
| Sat, 29 May 2004 14:55:56 +0200 |
wenzelm |
'classrel': support multiple arguments;
|
changeset |
files
|
| Sat, 29 May 2004 14:54:58 +0200 |
wenzelm |
* ML: all output via channels of writeln etc. passed through Output.output;
|
changeset |
files
|
| Sat, 29 May 2004 14:54:10 +0200 |
wenzelm |
output channels;
|
changeset |
files
|
| Fri, 28 May 2004 21:09:56 +0200 |
schirmer |
added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs
|
changeset |
files
|
| Fri, 28 May 2004 11:20:04 +0200 |
paulson |
new skolemize_tac and skolemize method
|
changeset |
files
|
| Fri, 28 May 2004 11:19:15 +0200 |
paulson |
new theorem Collect_imp_eq
|
changeset |
files
|
| Wed, 26 May 2004 19:06:09 +0200 |
chaieb |
abstraction over functions is no default any more.
|
changeset |
files
|
| Wed, 26 May 2004 18:52:18 +0200 |
webertj |
adjusted for different signature of Type.typ_instance
|
changeset |
files
|
| Wed, 26 May 2004 18:23:46 +0200 |
webertj |
mainly new/different datatype examples
|
changeset |
files
|
| Wed, 26 May 2004 18:06:38 +0200 |
webertj |
documentation updated
|
changeset |
files
|
| Wed, 26 May 2004 18:03:52 +0200 |
webertj |
major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
|
changeset |
files
|
| Wed, 26 May 2004 17:43:52 +0200 |
webertj |
new default parameters for refute
|
changeset |
files
|
| Wed, 26 May 2004 17:42:46 +0200 |
webertj |
solver "auto" now issues a warning when it uses solver "enumerate"
|
changeset |
files
|
| Wed, 26 May 2004 14:57:06 +0200 |
nipkow |
Corrected printer bug for bounded quantifiers Q x<=y. P
|
changeset |
files
|
| Wed, 26 May 2004 11:43:50 +0200 |
paulson |
more group isomorphisms
|
changeset |
files
|
| Mon, 24 May 2004 18:35:34 +0200 |
nipkow |
added drop_take:thm
|
changeset |
files
|
| Fri, 21 May 2004 21:49:45 +0200 |
berghofe |
- deleted unneeded function eta_long (now in Pure/pattern.ML
|
changeset |
files
|
| Fri, 21 May 2004 21:48:35 +0200 |
berghofe |
Adapted to new syntax for case expressions.
|
changeset |
files
|
| Fri, 21 May 2004 21:48:03 +0200 |
berghofe |
Added more flexible parse / print translations for case expressions.
|
changeset |
files
|
| Fri, 21 May 2004 21:47:07 +0200 |
berghofe |
Modified functions pt_to_ast and ast_to_term to improve handling
|
changeset |
files
|
| Fri, 21 May 2004 21:46:25 +0200 |
berghofe |
- exported result datatype
|
changeset |
files
|
| Fri, 21 May 2004 21:42:05 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Fri, 21 May 2004 21:28:58 +0200 |
wenzelm |
Pure: clear separation of logical types and nonterminals;
|
changeset |
files
|
| Fri, 21 May 2004 21:28:14 +0200 |
wenzelm |
adapted tsig/sg interface;
|
changeset |
files
|
| Fri, 21 May 2004 21:28:01 +0200 |
wenzelm |
added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
|
changeset |
files
|
| Fri, 21 May 2004 21:27:42 +0200 |
wenzelm |
added fold, product; removed transitive_closure;
|
changeset |
files
|
| Fri, 21 May 2004 21:27:10 +0200 |
wenzelm |
adapted names of some sort ops;
|
changeset |
files
|
| Fri, 21 May 2004 21:26:19 +0200 |
wenzelm |
major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
|
changeset |
files
|
| Fri, 21 May 2004 21:25:57 +0200 |
wenzelm |
Type.strip_sorts;
|
changeset |
files
|
| Fri, 21 May 2004 21:25:34 +0200 |
wenzelm |
incorporate type inference interface from type.ML;
|
changeset |
files
|
| Fri, 21 May 2004 21:24:22 +0200 |
wenzelm |
adapted tsig interface;
|
changeset |
files
|
| Fri, 21 May 2004 21:23:37 +0200 |
wenzelm |
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
|
changeset |
files
|
| Fri, 21 May 2004 21:23:12 +0200 |
wenzelm |
test_classrel/arity improve error reporting; tuned;
|
changeset |
files
|
| Fri, 21 May 2004 21:22:42 +0200 |
wenzelm |
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
|
changeset |
files
|
| Fri, 21 May 2004 21:22:10 +0200 |
wenzelm |
string_of_vname moved to term.ML;
|
changeset |
files
|
| Fri, 21 May 2004 21:21:51 +0200 |
wenzelm |
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
|
changeset |
files
|
| Fri, 21 May 2004 21:21:38 +0200 |
wenzelm |
type.ML now before Syntax module;
|
changeset |
files
|
| Fri, 21 May 2004 21:21:12 +0200 |
wenzelm |
xxx_typ_raw replace xxx_typ_no_norm forms;
|
changeset |
files
|