Wed, 02 Nov 2005 23:59:49 +0100 huffman fix spelling
Wed, 02 Nov 2005 16:37:39 +0100 berghofe Moved atom stuff to new file nominal_atoms.ML
Wed, 02 Nov 2005 15:31:12 +0100 urbanc - completed the list of thms for supp_atm
Wed, 02 Nov 2005 15:05:22 +0100 berghofe Added code for proving that new datatype has finite support.
Wed, 02 Nov 2005 14:48:55 +0100 wenzelm removed unused modify_typargs, map_typargs, fold_typargs;
Wed, 02 Nov 2005 14:47:01 +0100 wenzelm added Isar.state/exn;
Wed, 02 Nov 2005 14:47:00 +0100 wenzelm Isar.loop;
Wed, 02 Nov 2005 14:46:58 +0100 wenzelm moved consts declarations to consts.ML;
Wed, 02 Nov 2005 14:46:57 +0100 wenzelm Consts.dest;
Wed, 02 Nov 2005 14:46:56 +0100 wenzelm Polymorphic constants.
Wed, 02 Nov 2005 14:46:54 +0100 wenzelm added consts.ML;
Wed, 02 Nov 2005 14:46:53 +0100 wenzelm fromConst: use Sign.const_typargs for efficient representation of type instances of constant declarations;
Wed, 02 Nov 2005 14:46:51 +0100 wenzelm dist_eqI: the_context();
Wed, 02 Nov 2005 14:46:49 +0100 wenzelm Sign.const_monomorphic;
Wed, 02 Nov 2005 14:46:47 +0100 wenzelm Logic.nth_prem;
Wed, 02 Nov 2005 11:02:29 +0100 urbanc added the collection of lemmas "supp_at"
Tue, 01 Nov 2005 23:55:53 +0100 urbanc some minor tweaks in some proofs (nothing extraordinary)
Tue, 01 Nov 2005 23:54:29 +0100 urbanc tunings of some comments (nothing serious)
Mon, 31 Oct 2005 16:35:15 +0100 haftmann nth_*, fold_index refined
Mon, 31 Oct 2005 16:00:15 +0100 haftmann fold_index replacing foldln
Mon, 31 Oct 2005 01:43:22 +0100 nipkow A few new lemmas
Sun, 30 Oct 2005 10:55:56 +0100 urbanc tuned my last commit
Sun, 30 Oct 2005 10:37:57 +0100 urbanc simplified the abs_supp_approx proof and tuned some comments in
Sat, 29 Oct 2005 15:01:25 +0200 urbanc Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
Sat, 29 Oct 2005 14:37:32 +0200 urbanc 1) have adjusted the swapping of the result type
Fri, 28 Oct 2005 22:37:57 +0200 wenzelm tuned;
Fri, 28 Oct 2005 22:32:55 +0200 wenzelm lthms_containing: not o valid_thms;
Fri, 28 Oct 2005 22:28:15 +0200 wenzelm added fact_tac, some_fact_tac;
Fri, 28 Oct 2005 22:28:13 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:28:12 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:28:11 +0200 wenzelm added fact method;
Fri, 28 Oct 2005 22:28:09 +0200 wenzelm tuned ProofContext.export interfaces;
Fri, 28 Oct 2005 22:28:07 +0200 wenzelm syntax for literal facts;
Fri, 28 Oct 2005 22:28:06 +0200 wenzelm removed try_dest_Goal, use Logic.unprotect;
Fri, 28 Oct 2005 22:28:04 +0200 wenzelm added cgoal_of;
Fri, 28 Oct 2005 22:28:03 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 28 Oct 2005 22:28:02 +0200 wenzelm export cong_modifiers, simp_modifiers';
Fri, 28 Oct 2005 22:28:00 +0200 wenzelm certify_term: tuned monomorphic consts;
Fri, 28 Oct 2005 22:27:59 +0200 wenzelm datatype thmref: added Fact;
Fri, 28 Oct 2005 22:27:58 +0200 wenzelm Logic.lift_all;
Fri, 28 Oct 2005 22:27:57 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:27:56 +0200 wenzelm renamed Goal.norm_hhf_rule to Goal.norm_hhf;
Fri, 28 Oct 2005 22:27:55 +0200 wenzelm renamed Goal constant to prop, more general protect/unprotect interfaces;
Fri, 28 Oct 2005 22:27:54 +0200 wenzelm added add_local/add_global;
Fri, 28 Oct 2005 22:27:52 +0200 wenzelm added incr_indexes;
Fri, 28 Oct 2005 22:27:51 +0200 wenzelm renamed Goal constant to prop;
Fri, 28 Oct 2005 22:27:47 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 28 Oct 2005 22:27:46 +0200 wenzelm Logic.unprotect;
Fri, 28 Oct 2005 22:27:44 +0200 wenzelm literal facts;
Fri, 28 Oct 2005 22:27:41 +0200 wenzelm * Pure/Isar: literal facts;
Fri, 28 Oct 2005 22:26:10 +0200 wenzelm tuned;
Fri, 28 Oct 2005 20:18:37 +0200 webertj unnecessary imports removed
Fri, 28 Oct 2005 18:53:26 +0200 urbanc fixed case names in the weak induction principle and
Fri, 28 Oct 2005 18:22:26 +0200 berghofe Implemented proof of weak induction theorem.
Fri, 28 Oct 2005 17:59:07 +0200 berghofe Added "deepen" method.
Fri, 28 Oct 2005 17:27:49 +0200 haftmann circumvented smlnj value restriction
Fri, 28 Oct 2005 17:27:04 +0200 haftmann added extraction interface for code generator
Fri, 28 Oct 2005 16:43:46 +0200 urbanc Added (optional) arguments to the tactics
Fri, 28 Oct 2005 16:35:40 +0200 haftmann cleaned up nth, nth_update, nth_map and nth_string functions
Fri, 28 Oct 2005 13:52:57 +0200 berghofe Removed legacy prove_goalw_cterm command.
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip