Tue, 01 Jun 2004 12:33:50 +0200 wenzelm removed obsolete sort 'logic';
Tue, 01 Jun 2004 11:25:26 +0200 paulson more on bij_betw
Tue, 01 Jun 2004 11:25:01 +0200 paulson tidied
Tue, 01 Jun 2004 00:26:13 +0200 webertj TimeLimit structure added (no proper implementation yet)
Tue, 01 Jun 2004 00:18:01 +0200 webertj including polyml-time-limit.ML
Tue, 01 Jun 2004 00:17:07 +0200 webertj SML/NJs TimeLimit structure ported to Poly/ML
Mon, 31 May 2004 08:53:23 +0200 wenzelm oops -- no Output.out here;
Sat, 29 May 2004 16:50:53 +0200 wenzelm updated;
Sat, 29 May 2004 16:47:06 +0200 wenzelm \<^bsub>/\<^esub> syntax: unbreakable block;
Sat, 29 May 2004 15:11:43 +0200 wenzelm \<^bsub>/\<^esub> syntax: unbreakable block;
Sat, 29 May 2004 15:11:06 +0200 wenzelm Scan.this; tuned;
Sat, 29 May 2004 15:10:56 +0200 wenzelm do *not* export list/list1 -- commas considered special in arg syntax;
Sat, 29 May 2004 15:10:30 +0200 wenzelm target 'generate';
Sat, 29 May 2004 15:09:47 +0200 wenzelm avoid Args.list;
Sat, 29 May 2004 15:08:21 +0200 wenzelm handle raw symbols; Output.add_mode;
Sat, 29 May 2004 15:08:08 +0200 wenzelm handle raw symbols; Output.add_mode; more robust handling of sub/superscript;
Sat, 29 May 2004 15:07:42 +0200 wenzelm tuned _dummy_ofsort syntax;
Sat, 29 May 2004 15:07:29 +0200 wenzelm added pp_show_brackets; support unbreakable blocks;
Sat, 29 May 2004 15:07:05 +0200 wenzelm transform_error;
Sat, 29 May 2004 15:06:42 +0200 wenzelm Library.read_int; Output.output;
Sat, 29 May 2004 15:06:19 +0200 wenzelm improved support for raw symbols;
Sat, 29 May 2004 15:06:04 +0200 wenzelm Output.error;
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;
Sat, 29 May 2004 15:05:37 +0200 wenzelm added Pure/General/output.ML; load Pure/General/pretty.ML early in Pure/ROOT.ML;
Sat, 29 May 2004 15:05:25 +0200 wenzelm removed norm_typ; improved output; refer to Pretty.pp;
Sat, 29 May 2004 15:05:02 +0200 wenzelm moved read_int etc. to library.ML; added type 'arity';
Sat, 29 May 2004 15:03:59 +0200 wenzelm improved output; refer to Pretty.pp;
Sat, 29 May 2004 15:02:35 +0200 wenzelm Output.add_mode; Output.timing;
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;
Sat, 29 May 2004 15:01:36 +0200 wenzelm Output.timing;
Sat, 29 May 2004 15:00:52 +0200 wenzelm improved output;
Sat, 29 May 2004 15:00:25 +0200 wenzelm moved print_mode to General/output.ML; load General/pretty.ML early;
Sat, 29 May 2004 15:00:14 +0200 wenzelm added Pure/General/output.ML;
Sat, 29 May 2004 14:59:57 +0200 wenzelm avoid 'handle _' -- would cover Interrupt as well!!!
Sat, 29 May 2004 14:59:24 +0200 wenzelm Sign.infer_types: Sign.pp;
Sat, 29 May 2004 14:58:44 +0200 wenzelm Library.read_int;
Sat, 29 May 2004 14:57:39 +0200 wenzelm Output.output;
Sat, 29 May 2004 14:55:56 +0200 wenzelm 'classrel': support multiple arguments;
Sat, 29 May 2004 14:54:58 +0200 wenzelm * ML: all output via channels of writeln etc. passed through Output.output;
Sat, 29 May 2004 14:54:10 +0200 wenzelm output channels;
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
Fri, 28 May 2004 11:20:04 +0200 paulson new skolemize_tac and skolemize method
Fri, 28 May 2004 11:19:15 +0200 paulson new theorem Collect_imp_eq
Wed, 26 May 2004 19:06:09 +0200 chaieb abstraction over functions is no default any more.
Wed, 26 May 2004 18:52:18 +0200 webertj adjusted for different signature of Type.typ_instance
Wed, 26 May 2004 18:23:46 +0200 webertj mainly new/different datatype examples
Wed, 26 May 2004 18:06:38 +0200 webertj documentation updated
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)
Wed, 26 May 2004 17:43:52 +0200 webertj new default parameters for refute
Wed, 26 May 2004 17:42:46 +0200 webertj solver "auto" now issues a warning when it uses solver "enumerate"
Wed, 26 May 2004 14:57:06 +0200 nipkow Corrected printer bug for bounded quantifiers Q x<=y. P
Wed, 26 May 2004 11:43:50 +0200 paulson more group isomorphisms
Mon, 24 May 2004 18:35:34 +0200 nipkow added drop_take:thm
Fri, 21 May 2004 21:49:45 +0200 berghofe - deleted unneeded function eta_long (now in Pure/pattern.ML
Fri, 21 May 2004 21:48:35 +0200 berghofe Adapted to new syntax for case expressions.
Fri, 21 May 2004 21:48:03 +0200 berghofe Added more flexible parse / print translations for case expressions.
Fri, 21 May 2004 21:47:07 +0200 berghofe Modified functions pt_to_ast and ast_to_term to improve handling
Fri, 21 May 2004 21:46:25 +0200 berghofe - exported result datatype
Fri, 21 May 2004 21:42:05 +0200 wenzelm updated;
Fri, 21 May 2004 21:28:58 +0200 wenzelm Pure: clear separation of logical types and nonterminals;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip