Tue, 08 Nov 2005 15:26:35 +0100 haftmann allowing indentation of 'theory' keyword
Tue, 08 Nov 2005 10:44:40 +0100 wenzelm simplified after_qed;
Tue, 08 Nov 2005 10:43:15 +0100 wenzelm avoid prove_plain, export_plain, simplified after_qed;
Tue, 08 Nov 2005 10:43:13 +0100 wenzelm removed export_plain;
Tue, 08 Nov 2005 10:43:12 +0100 wenzelm renamed assert_prop to ensure_prop;
Tue, 08 Nov 2005 10:43:11 +0100 wenzelm renamed goals.ML to old_goals.ML;
Tue, 08 Nov 2005 10:43:10 +0100 wenzelm export compose_hhf;
Tue, 08 Nov 2005 10:43:09 +0100 wenzelm removed impose_hyps, satisfy_hyps;
Tue, 08 Nov 2005 10:43:08 +0100 wenzelm const args: do not store variable names (unused);
Tue, 08 Nov 2005 10:43:05 +0100 wenzelm renamed goals.ML to old_goals.ML;
Tue, 08 Nov 2005 09:13:22 +0100 haftmann (fix for accidental commit)
Tue, 08 Nov 2005 09:12:02 +0100 haftmann (codegen)
Tue, 08 Nov 2005 02:19:11 +0100 huffman generate pattern combinators for new datatypes
Mon, 07 Nov 2005 23:33:01 +0100 huffman reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
Mon, 07 Nov 2005 23:30:49 +0100 huffman add case syntax for type one
Mon, 07 Nov 2005 19:23:53 +0100 huffman remove syntax for as-patterns
Mon, 07 Nov 2005 19:03:02 +0100 wenzelm avoid 'as' as identifier;
Mon, 07 Nov 2005 18:50:53 +0100 wenzelm avoid 'as' as identifier;
Mon, 07 Nov 2005 18:32:54 +0100 berghofe Added strong induction theorem (currently only axiomatized!).
Mon, 07 Nov 2005 15:19:03 +0100 urbanc Initial commit.
Mon, 07 Nov 2005 15:12:13 +0100 urbanc Initial commit of the theory "Weakening".
Mon, 07 Nov 2005 14:35:25 +0100 urbanc added thms perm, distinct and fresh to the simplifier.
Mon, 07 Nov 2005 12:06:11 +0100 haftmann added proper fillin_mixfix
Mon, 07 Nov 2005 11:39:24 +0100 haftmann added fillin_mixfix, replace_quote
Mon, 07 Nov 2005 11:28:34 +0100 berghofe New function store_thmss_atts.
Mon, 07 Nov 2005 11:17:45 +0100 urbanc used the function Library.product for the cprod from Stefan
Mon, 07 Nov 2005 10:47:25 +0100 urbanc fixed bug with nominal induct
Mon, 07 Nov 2005 09:34:51 +0100 haftmann added fillin_mixfix' needed by serializer
Sun, 06 Nov 2005 01:21:37 +0100 huffman add case syntax stuff
Sun, 06 Nov 2005 00:35:24 +0100 huffman use consts for infix syntax
Sun, 06 Nov 2005 00:22:03 +0100 huffman add proof of Bekic's theorem: fix_cprod
Sat, 05 Nov 2005 21:56:45 +0100 huffman simplify definitions
Sat, 05 Nov 2005 21:52:13 +0100 huffman put iterate and fix in separate sections; added Letrec
Sat, 05 Nov 2005 21:50:37 +0100 huffman renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
Sat, 05 Nov 2005 21:42:24 +0100 huffman add line breaks to Rep_CFun syntax
Fri, 04 Nov 2005 23:15:45 +0100 huffman moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
Fri, 04 Nov 2005 23:15:11 +0100 huffman moved adm_chfindom from Fix.thy to Cfun.thy
Fri, 04 Nov 2005 22:27:40 +0100 huffman cleaned up
Fri, 04 Nov 2005 22:26:09 +0100 huffman add print translation: Abs_CFun f => LAM x. f x
Thu, 03 Nov 2005 04:31:12 +0100 mengj Changed the way additional lemmas are passed to ATP methods for proof of a goal: now only list them after the methods' names.
Thu, 03 Nov 2005 03:06:02 +0100 huffman improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
Thu, 03 Nov 2005 02:37:09 +0100 huffman reimplement copy_def to use data constructor constants
Thu, 03 Nov 2005 02:19:48 +0100 huffman cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
Thu, 03 Nov 2005 01:54:51 +0100 huffman generate lambda pattern syntax for new data constructors
Thu, 03 Nov 2005 01:45:52 +0100 huffman changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
Thu, 03 Nov 2005 01:44:27 +0100 huffman add constant one_when; LAM pattern for ONE
Thu, 03 Nov 2005 01:28:22 +0100 huffman add translation for wildcard pattern
Thu, 03 Nov 2005 01:11:39 +0100 huffman change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
Thu, 03 Nov 2005 01:02:29 +0100 huffman make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
Thu, 03 Nov 2005 00:57:35 +0100 huffman cleaned up; ch2ch_Rep_CFun is a simp rule
Thu, 03 Nov 2005 00:43:50 +0100 huffman changed iterate to a continuous type
Thu, 03 Nov 2005 00:43:11 +0100 huffman reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
Thu, 03 Nov 2005 00:32:47 +0100 huffman removed ex/loeckx.ML
Thu, 03 Nov 2005 00:31:32 +0100 huffman removed proof about Ifix, which no longer exists
Thu, 03 Nov 2005 00:16:09 +0100 huffman cleaned up; chain_const and thelub_const are simp rules
Thu, 03 Nov 2005 00:12:29 +0100 huffman cleaned up; removed adm_tricks in favor of compactness theorems
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.
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip