2004-05-31 wenzelm 2004-05-31 oops -- no Output.out here;
2004-05-29 wenzelm 2004-05-29 updated;
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-29 wenzelm 2004-05-29 \<^bsub>/\<^esub> syntax: unbreakable block;
2004-05-29 wenzelm 2004-05-29 Scan.this; tuned;
2004-05-29 wenzelm 2004-05-29 do *not* export list/list1 -- commas considered special in arg syntax;
2004-05-29 wenzelm 2004-05-29 target 'generate';
2004-05-29 wenzelm 2004-05-29 avoid Args.list;
2004-05-29 wenzelm 2004-05-29 handle raw symbols; Output.add_mode;
2004-05-29 wenzelm 2004-05-29 handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
2004-05-29 wenzelm 2004-05-29 tuned _dummy_ofsort syntax;
2004-05-29 wenzelm 2004-05-29 added pp_show_brackets; support unbreakable blocks;
2004-05-29 wenzelm 2004-05-29 transform_error;
2004-05-29 wenzelm 2004-05-29 Library.read_int; Output.output;
2004-05-29 wenzelm 2004-05-29 improved support for raw symbols;
2004-05-29 wenzelm 2004-05-29 Output.error;
2004-05-29 wenzelm 2004-05-29 pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
2004-05-29 wenzelm 2004-05-29 added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
2004-05-29 wenzelm 2004-05-29 removed norm_typ; improved output; refer to Pretty.pp;
2004-05-29 wenzelm 2004-05-29 moved read_int etc. to library.ML; added type 'arity';
2004-05-29 wenzelm 2004-05-29 improved output; refer to Pretty.pp;
2004-05-29 wenzelm 2004-05-29 Output.add_mode; Output.timing;
2004-05-29 wenzelm 2004-05-29 output channels and diagnostics moved to General/output.ML; added read_int etc. from term.ML; removed obsolete mtree; type rat uses exception RAT;
2004-05-29 wenzelm 2004-05-29 Output.timing;
2004-05-29 wenzelm 2004-05-29 improved output;
2004-05-29 wenzelm 2004-05-29 moved print_mode to General/output.ML; load General/pretty.ML early;
2004-05-29 wenzelm 2004-05-29 added Pure/General/output.ML;
2004-05-29 wenzelm 2004-05-29 avoid 'handle _' -- would cover Interrupt as well!!!
2004-05-29 wenzelm 2004-05-29 Sign.infer_types: Sign.pp;
2004-05-29 wenzelm 2004-05-29 Library.read_int;
2004-05-29 wenzelm 2004-05-29 Output.output;
2004-05-29 wenzelm 2004-05-29 'classrel': support multiple arguments;
2004-05-29 wenzelm 2004-05-29 * ML: all output via channels of writeln etc. passed through Output.output;
2004-05-29 wenzelm 2004-05-29 output channels;
2004-05-28 schirmer 2004-05-28 added asm_lr_simplify/asm_lr_rewrite and adapted asm_full_simplify/asm_full_rewrite to match to corresponding simp_tacs
2004-05-28 paulson 2004-05-28 new skolemize_tac and skolemize method
2004-05-28 paulson 2004-05-28 new theorem Collect_imp_eq
2004-05-26 chaieb 2004-05-26 abstraction over functions is no default any more.
2004-05-26 webertj 2004-05-26 adjusted for different signature of Type.typ_instance
2004-05-26 webertj 2004-05-26 mainly new/different datatype examples
2004-05-26 webertj 2004-05-26 documentation updated
2004-05-26 webertj 2004-05-26 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)
2004-05-26 webertj 2004-05-26 new default parameters for refute
2004-05-26 webertj 2004-05-26 solver "auto" now issues a warning when it uses solver "enumerate"
2004-05-26 nipkow 2004-05-26 Corrected printer bug for bounded quantifiers Q x<=y. P
2004-05-26 paulson 2004-05-26 more group isomorphisms
2004-05-24 nipkow 2004-05-24 added drop_take:thm
2004-05-21 berghofe 2004-05-21 - deleted unneeded function eta_long (now in Pure/pattern.ML - added HOL.min / HOL.max to allowed consts again - added final simplification step with presburger_ss to preprocessor again
2004-05-21 berghofe 2004-05-21 Adapted to new syntax for case expressions.
2004-05-21 berghofe 2004-05-21 Added more flexible parse / print translations for case expressions.
2004-05-21 berghofe 2004-05-21 Modified functions pt_to_ast and ast_to_term to improve handling of errors in parse (ast) translations caused by ambiguous input.
2004-05-21 berghofe 2004-05-21 - exported result datatype - added functions get_result and get_exn
2004-05-21 wenzelm 2004-05-21 updated;
2004-05-21 wenzelm 2004-05-21 Pure: clear separation of logical types and nonterminals;
2004-05-21 wenzelm 2004-05-21 adapted tsig/sg interface;
2004-05-21 wenzelm 2004-05-21 added dest, minimals, maximals, is_edge, add_edge/merge_trans_acyclic;
2004-05-21 wenzelm 2004-05-21 added fold, product; removed transitive_closure;
2004-05-21 wenzelm 2004-05-21 adapted names of some sort ops;
2004-05-21 wenzelm 2004-05-21 major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
2004-05-21 wenzelm 2004-05-21 Type.strip_sorts;