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;
Wed, 29 Jun 2005 15:13:35 +0200 wenzelm added print_mode three_buffersN and corresponding cond_print;
Wed, 29 Jun 2005 15:13:34 +0200 wenzelm cond_print for end-of-proof and calculational commands;
Wed, 29 Jun 2005 15:13:33 +0200 wenzelm added eq;
Wed, 29 Jun 2005 15:13:32 +0200 wenzelm pass thy as explicit argument (the old ref was not safe
Wed, 29 Jun 2005 15:13:31 +0200 wenzelm more efficient treatment of shyps and hyps (use ordered lists);
Wed, 29 Jun 2005 15:13:30 +0200 wenzelm Syntax.read thy;
Wed, 29 Jun 2005 15:13:29 +0200 wenzelm tuned sort_ord: pointer_eq;
Wed, 29 Jun 2005 15:13:28 +0200 wenzelm removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort;
Wed, 29 Jun 2005 15:13:27 +0200 wenzelm eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;
Wed, 29 Jun 2005 15:13:26 +0200 wenzelm replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);
Wed, 29 Jun 2005 15:13:25 +0200 wenzelm added implies_intr_hyps (from thm.ML);
Wed, 29 Jun 2005 15:13:23 +0200 wenzelm added joinable;
Tue, 28 Jun 2005 17:56:04 +0200 paulson stylistic improvements
Tue, 28 Jun 2005 16:12:03 +0200 haftmann added project information in overview
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip