Fri, 01 Jul 2005 22:33:59 +0200 wenzelm decomp_simp: compare terms, not cterms;
Fri, 01 Jul 2005 22:29:19 +0200 wenzelm back to 1.28;
Fri, 01 Jul 2005 17:41:10 +0200 nipkow prime is a predicate now.
Fri, 01 Jul 2005 14:55:05 +0200 wenzelm * Isar profiling: new reference Toplevel.profiling (default 0);
Fri, 01 Jul 2005 14:42:05 +0200 wenzelm use tracing for potentially voluminous ambiguity output;
Fri, 01 Jul 2005 14:42:04 +0200 wenzelm added profiler interface (dummy);
Fri, 01 Jul 2005 14:42:03 +0200 wenzelm added profiler interface, keep 'profiling' of PolyML structure;
Fri, 01 Jul 2005 14:42:02 +0200 wenzelm added profile flag;
Fri, 01 Jul 2005 14:42:01 +0200 wenzelm low-level tuning of map, fold;
Fri, 01 Jul 2005 14:42:00 +0200 wenzelm ctyp: added 'sorts' field;
Fri, 01 Jul 2005 14:41:59 +0200 wenzelm added all_sorts_nonempty;
Fri, 01 Jul 2005 14:41:58 +0200 wenzelm low-level tuning of fold, fold_rev, foldl_map;
Fri, 01 Jul 2005 14:41:57 +0200 wenzelm isatool install: removed KDE option;
Fri, 01 Jul 2005 14:22:33 +0200 berghofe Fixed bug: lookup' must use = instead of eq_type to compare types of
Fri, 01 Jul 2005 14:20:01 +0200 berghofe Changed interface of Envir.lookup'
Fri, 01 Jul 2005 14:19:36 +0200 berghofe Moved eq_type from envir.ML to type.ML
Fri, 01 Jul 2005 14:18:27 +0200 berghofe Implemented modular code generation.
Fri, 01 Jul 2005 14:17:32 +0200 berghofe Simplified proof (thanks to strengthened ball_cong).
Fri, 01 Jul 2005 14:16:32 +0200 berghofe Proof of wx_ex_prop must now use old bex_cong to prevent simplifier from looping.
Fri, 01 Jul 2005 14:14:40 +0200 berghofe Adapted to new interface of RecfunCodegen.add.
Fri, 01 Jul 2005 14:13:40 +0200 berghofe Adapted to modular code generation.
Fri, 01 Jul 2005 14:11:06 +0200 berghofe Corrected implementation of arbitrary on cname.
Fri, 01 Jul 2005 14:10:02 +0200 berghofe Added BasisLibrary prefix to List.concat to avoid problems with
Fri, 01 Jul 2005 14:08:53 +0200 berghofe Moved code generator setup from NatBin to IntDef.
Fri, 01 Jul 2005 14:06:57 +0200 berghofe Simplified some proofs (thanks to strong_setsum_cong).
Fri, 01 Jul 2005 14:05:41 +0200 berghofe Removed setsubgoaler hack (thanks to strong_setsum_cong).
Fri, 01 Jul 2005 14:03:50 +0200 berghofe Removed setsubgoaler hack (thanks to strengthened finsum_cong).
Fri, 01 Jul 2005 14:02:58 +0200 berghofe Removed setsubgoaler hack.
Fri, 01 Jul 2005 14:01:13 +0200 berghofe Tuned finsum_cong to allow that premises are simplified more eagerly.
Fri, 01 Jul 2005 13:57:53 +0200 berghofe Added strong_ball_cong and strong_bex_cong (these are now the standard
Fri, 01 Jul 2005 13:56:34 +0200 berghofe Moved some code lemmas from Main to Nat.
Fri, 01 Jul 2005 13:54:57 +0200 berghofe Adapted to new interface of code generator.
Fri, 01 Jul 2005 13:54:12 +0200 berghofe Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
Fri, 01 Jul 2005 13:51:11 +0200 berghofe Added strong_setsum_cong and strong_setprod_cong.
Fri, 01 Jul 2005 04:32:33 +0200 huffman defaultsort pcpo
Fri, 01 Jul 2005 04:09:27 +0200 huffman added theorem lift_definedE; moved cont_if to Cont.thy
Fri, 01 Jul 2005 04:02:22 +0200 huffman added tactic cont_tac
Fri, 01 Jul 2005 04:00:23 +0200 huffman remove uses of sign_of
Fri, 01 Jul 2005 02:35:24 +0200 huffman cleaned up
Fri, 01 Jul 2005 02:30:59 +0200 huffman cleaned up
Fri, 01 Jul 2005 01:50:46 +0200 huffman renamed flatdom2monofun to flatdom_strict2mono
Fri, 01 Jul 2005 01:50:07 +0200 huffman cleaned up; reorganized and added section headings
Fri, 01 Jul 2005 01:48:37 +0200 huffman cleaned up; added adm_less to adm_lemmas; added subsection headings
Thu, 30 Jun 2005 19:49:41 +0200 wenzelm revert to 1.27 due to obscure performance issues (!??);
Thu, 30 Jun 2005 19:43:50 +0200 huffman replace filter2 with List.partition
Thu, 30 Jun 2005 14:06:29 +0200 ballarin Proper treatment of beta-redexes in witness theorems.
Thu, 30 Jun 2005 08:57:53 +0200 haftmann minor corrections
Thu, 30 Jun 2005 08:23:47 +0200 kleing test sml-dev on mac as well
Thu, 30 Jun 2005 08:23:20 +0200 kleing use only 1 CPU on MacOS 10.4.1
Thu, 30 Jun 2005 08:22:56 +0200 kleing use kleing@cse instead of kleing@in.tum.de
Thu, 30 Jun 2005 05:27:40 +0200 kleing use global settings for isatest-doc
Wed, 29 Jun 2005 15:13:44 +0200 wenzelm export no_type_brackets;
Wed, 29 Jun 2005 15:13:43 +0200 wenzelm proper treatment of advanced trfuns: pass thy argument;
Wed, 29 Jun 2005 15:13:42 +0200 wenzelm transform_failure in translation functions: TRANSLATION_FAIL;
Wed, 29 Jun 2005 15:13:41 +0200 wenzelm proper treatment of advanced trfuns: pass thy argument;
Wed, 29 Jun 2005 15:13:40 +0200 wenzelm accomodate advanced trfuns;
Wed, 29 Jun 2005 15:13:39 +0200 wenzelm removed obsolete (un)fold_ast2;
Wed, 29 Jun 2005 15:13:38 +0200 wenzelm Drule.implies_intr_hyps;
Wed, 29 Jun 2005 15:13:37 +0200 wenzelm added print': print depending on print_mode;
Wed, 29 Jun 2005 15:13:36 +0200 wenzelm no Syntax.internal on thesis;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip