2011-12-16 merged
nipkow [Fri, 16 Dec 2011 12:01:10 +0100] rev 45904
merged
2011-12-16 improved indexed complete lattice
nipkow [Fri, 16 Dec 2011 12:00:59 +0100] rev 45903
improved indexed complete lattice
2011-12-16 more elementary defs;
wenzelm [Fri, 16 Dec 2011 22:08:48 +0100] rev 45902
more elementary defs;
2011-12-16 eliminated old-fashioned Global_Theory.add_thms(s);
wenzelm [Fri, 16 Dec 2011 21:23:21 +0100] rev 45901
eliminated old-fashioned Global_Theory.add_thms(s);
2011-12-16 prefer sorting from Scala library;
wenzelm [Fri, 16 Dec 2011 13:37:08 +0100] rev 45900
prefer sorting from Scala library;
2011-12-16 prefer Name.context operations;
wenzelm [Fri, 16 Dec 2011 12:03:33 +0100] rev 45899
prefer Name.context operations;
2011-12-16 tuned;
wenzelm [Fri, 16 Dec 2011 11:02:55 +0100] rev 45898
tuned;
2011-12-16 clarified modules that contribute to datatype package;
wenzelm [Fri, 16 Dec 2011 10:52:35 +0100] rev 45897
clarified modules that contribute to datatype package;
2011-12-16 tuned signature;
wenzelm [Fri, 16 Dec 2011 10:38:38 +0100] rev 45896
tuned signature;
2011-12-15 merged;
wenzelm [Thu, 15 Dec 2011 21:46:52 +0100] rev 45895
merged;
2011-12-15 tuned;
wenzelm [Thu, 15 Dec 2011 19:53:28 +0100] rev 45894
tuned;
2011-12-15 add complementary lemmas for {min,max}_least
noschinl [Thu, 15 Dec 2011 16:10:44 +0100] rev 45893
add complementary lemmas for {min,max}_least
2011-12-15 add lemmas about limits
noschinl [Thu, 15 Dec 2011 15:55:39 +0100] rev 45892
add lemmas about limits
2011-12-15 clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
wenzelm [Thu, 15 Dec 2011 18:08:40 +0100] rev 45891
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
2011-12-15 separate rep_datatype.ML;
wenzelm [Thu, 15 Dec 2011 17:37:14 +0100] rev 45890
separate rep_datatype.ML; tuned signature;
2011-12-15 misc tuning and simplification;
wenzelm [Thu, 15 Dec 2011 14:11:57 +0100] rev 45889
misc tuning and simplification;
2011-12-15 more stats;
wenzelm [Thu, 15 Dec 2011 13:40:20 +0100] rev 45888
more stats;
2011-12-15 made SML/NJ happier
blanchet [Thu, 15 Dec 2011 10:38:50 +0100] rev 45887
made SML/NJ happier
2011-12-15 merged
nipkow [Thu, 15 Dec 2011 09:13:32 +0100] rev 45886
merged
2011-12-15 tuned
nipkow [Thu, 15 Dec 2011 09:13:23 +0100] rev 45885
tuned
2011-12-15 hiding the precious name map_entry in AList_Impl
bulwahn [Thu, 15 Dec 2011 08:51:14 +0100] rev 45884
hiding the precious name map_entry in AList_Impl
2011-12-14 killed dead code
blanchet [Wed, 14 Dec 2011 23:08:03 +0100] rev 45883
killed dead code
2011-12-14 use new redirection algorithm in Sledgehammer
blanchet [Wed, 14 Dec 2011 23:08:03 +0100] rev 45882
use new redirection algorithm in Sledgehammer
2011-12-14 fixed parsing of TPTP atoms
blanchet [Wed, 14 Dec 2011 23:08:03 +0100] rev 45881
fixed parsing of TPTP atoms
2011-12-14 tuned signature;
wenzelm [Wed, 14 Dec 2011 22:10:04 +0100] rev 45880
tuned signature;
2011-12-14 avoid fragile Sign.intern_const -- pass internal names directly;
wenzelm [Wed, 14 Dec 2011 21:54:32 +0100] rev 45879
avoid fragile Sign.intern_const -- pass internal names directly; tuned;
2011-12-14 tuned;
wenzelm [Wed, 14 Dec 2011 20:36:17 +0100] rev 45878
tuned;
2011-12-14 added new proof redirection code
blanchet [Wed, 14 Dec 2011 18:07:32 +0100] rev 45877
added new proof redirection code
2011-12-14 SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite
blanchet [Wed, 14 Dec 2011 18:07:32 +0100] rev 45876
SPASS is incomplete because of the -Splits and -FullRed options, not just because of -SOS=1 -- don't pretend the opposite
2011-12-14 make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)
blanchet [Wed, 14 Dec 2011 18:07:32 +0100] rev 45875
make sure that all symbols are declared in untyped SPASS DFG output (broken since 3b8606fba2dd)
2011-12-14 NEWS
bulwahn [Wed, 14 Dec 2011 17:49:42 +0100] rev 45874
NEWS
2011-12-14 correcting dependencies after renaming
bulwahn [Wed, 14 Dec 2011 16:30:32 +0100] rev 45873
correcting dependencies after renaming
2011-12-14 tuned header after renaming
bulwahn [Wed, 14 Dec 2011 16:30:30 +0100] rev 45872
tuned header after renaming
2011-12-14 moving AList theory to AList_Impl to make space for the association lists with invariant
bulwahn [Wed, 14 Dec 2011 16:30:29 +0100] rev 45871
moving AList theory to AList_Impl to make space for the association lists with invariant
2011-12-14 merged
bulwahn [Wed, 14 Dec 2011 16:30:09 +0100] rev 45870
merged
2011-12-14 adding map_entry to AList theory
bulwahn [Wed, 14 Dec 2011 15:56:37 +0100] rev 45869
adding map_entry to AList theory
2011-12-14 adding map_default to AList theory
bulwahn [Wed, 14 Dec 2011 15:56:34 +0100] rev 45868
adding map_default to AList theory
2011-12-14 fixed typo in theorem name in AList theory
bulwahn [Wed, 14 Dec 2011 15:56:31 +0100] rev 45867
fixed typo in theorem name in AList theory
2011-12-14 adding code attribute to enable evaluation of equality on multisets
bulwahn [Wed, 14 Dec 2011 15:56:29 +0100] rev 45866
adding code attribute to enable evaluation of equality on multisets
2011-12-14 merged
wenzelm [Wed, 14 Dec 2011 15:50:15 +0100] rev 45865
merged
2011-12-14 updated Sledgehammer/SMT docs
blanchet [Wed, 14 Dec 2011 15:05:22 +0100] rev 45864
updated Sledgehammer/SMT docs
2011-12-14 tuned signature;
wenzelm [Wed, 14 Dec 2011 15:30:17 +0100] rev 45863
tuned signature;
2011-12-14 eliminated dead code;
wenzelm [Wed, 14 Dec 2011 12:18:19 +0100] rev 45862
eliminated dead code;
2011-12-14 some full isatest runs, which include benchmark targets;
wenzelm [Wed, 14 Dec 2011 12:10:44 +0100] rev 45861
some full isatest runs, which include benchmark targets;
2011-12-14 more visible benchmarks;
wenzelm [Wed, 14 Dec 2011 12:02:02 +0100] rev 45860
more visible benchmarks; uniform IsaMakefile target "full" to cover such extra sessions;
2011-12-14 fixed Nitpick definition of "<" on "real"s
blanchet [Wed, 14 Dec 2011 10:18:28 +0100] rev 45859
fixed Nitpick definition of "<" on "real"s
2011-12-14 replace 'lemmas' with 'lemma'
huffman [Wed, 14 Dec 2011 08:32:48 +0100] rev 45858
replace 'lemmas' with 'lemma'
2011-12-14 merged
huffman [Wed, 14 Dec 2011 07:38:30 +0100] rev 45857
merged
2011-12-13 more simp rules for sbintrunc
huffman [Tue, 13 Dec 2011 18:33:04 +0100] rev 45856
more simp rules for sbintrunc
2011-12-13 add simp rules for sbintrunc applied to numerals
huffman [Tue, 13 Dec 2011 15:34:59 +0100] rev 45855
add simp rules for sbintrunc applied to numerals
2011-12-13 replace many uses of 'lemmas' with explicit 'lemma'
huffman [Tue, 13 Dec 2011 14:39:14 +0100] rev 45854
replace many uses of 'lemmas' with explicit 'lemma'
2011-12-13 add lemma bin_nth_zero
huffman [Tue, 13 Dec 2011 14:02:02 +0100] rev 45853
add lemma bin_nth_zero
2011-12-13 add simp rules for bintrunc applied to numerals
huffman [Tue, 13 Dec 2011 19:21:36 +0100] rev 45852
add simp rules for bintrunc applied to numerals
2011-12-13 add simp rules for bin_rest and bin_last applied to numerals
huffman [Tue, 13 Dec 2011 13:21:48 +0100] rev 45851
add simp rules for bin_rest and bin_last applied to numerals
2011-12-13 add simp rules for bin_sign applied to numerals
huffman [Tue, 13 Dec 2011 13:10:25 +0100] rev 45850
add simp rules for bin_sign applied to numerals
2011-12-13 add simp rules for BIT applied to numerals
huffman [Tue, 13 Dec 2011 13:05:44 +0100] rev 45849
add simp rules for BIT applied to numerals
2011-12-13 declare BIT_eq_iff [iff]; remove unneeded lemmas
huffman [Tue, 13 Dec 2011 12:55:36 +0100] rev 45848
declare BIT_eq_iff [iff]; remove unneeded lemmas
2011-12-13 towards removing BIT_simps from the simpset
huffman [Tue, 13 Dec 2011 12:36:41 +0100] rev 45847
towards removing BIT_simps from the simpset
2011-12-13 type signature for bin_sign
huffman [Tue, 13 Dec 2011 12:10:43 +0100] rev 45846
type signature for bin_sign
2011-12-13 remove some unwanted numeral-representation-specific simp rules
huffman [Tue, 13 Dec 2011 12:05:47 +0100] rev 45845
remove some unwanted numeral-representation-specific simp rules
2011-12-13 remove redundant lemmas
huffman [Tue, 13 Dec 2011 11:48:59 +0100] rev 45844
remove redundant lemmas
2011-12-13 reorder some definitions and proofs, in preparation for new numeral representation
huffman [Tue, 13 Dec 2011 11:26:10 +0100] rev 45843
reorder some definitions and proofs, in preparation for new numeral representation
2011-12-13 merged
wenzelm [Tue, 13 Dec 2011 23:22:27 +0100] rev 45842
merged
2011-12-13 added lemmas
noschinl [Tue, 13 Dec 2011 22:44:16 +0100] rev 45841
added lemmas
2011-12-13 added concrete syntax
nipkow [Tue, 13 Dec 2011 21:15:38 +0100] rev 45840
added concrete syntax
2011-12-13 'datatype' specifications allow explicit sort constraints;
wenzelm [Tue, 13 Dec 2011 23:23:51 +0100] rev 45839
'datatype' specifications allow explicit sort constraints; tuned signatures;
2011-12-13 do not open ML structures;
wenzelm [Tue, 13 Dec 2011 20:29:59 +0100] rev 45838
do not open ML structures;
2011-12-13 tuned;
wenzelm [Tue, 13 Dec 2011 20:10:36 +0100] rev 45837
tuned;
2011-12-13 removed dead code;
wenzelm [Tue, 13 Dec 2011 20:10:28 +0100] rev 45836
removed dead code;
2011-12-13 comment;
wenzelm [Tue, 13 Dec 2011 20:10:11 +0100] rev 45835
comment;
2011-12-13 connect while_option with lfp
nipkow [Tue, 13 Dec 2011 16:53:28 +0100] rev 45834
connect while_option with lfp
2011-12-13 lemmas about Kleene iteration
nipkow [Tue, 13 Dec 2011 16:14:41 +0100] rev 45833
lemmas about Kleene iteration
2011-12-13 merged
wenzelm [Tue, 13 Dec 2011 15:19:30 +0100] rev 45832
merged
2011-12-13 avoid multiple type decls in TFF (improves on cef82dc1462d)
blanchet [Tue, 13 Dec 2011 14:55:42 +0100] rev 45831
avoid multiple type decls in TFF (improves on cef82dc1462d)
2011-12-13 added missing quantifier
blanchet [Tue, 13 Dec 2011 14:55:42 +0100] rev 45830
added missing quantifier
2011-12-13 remove needless declaration in TFF1 problems
blanchet [Tue, 13 Dec 2011 14:55:42 +0100] rev 45829
remove needless declaration in TFF1 problems
2011-12-13 correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
blanchet [Tue, 13 Dec 2011 14:55:42 +0100] rev 45828
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
2011-12-13 modernized specifications;
wenzelm [Tue, 13 Dec 2011 15:18:52 +0100] rev 45827
modernized specifications;
2011-12-13 support phantom types as quotient types
kuncar [Tue, 13 Dec 2011 14:04:20 +0100] rev 45826
support phantom types as quotient types
2011-12-12 merged
wenzelm [Mon, 12 Dec 2011 23:06:41 +0100] rev 45825
merged
2011-12-12 merged
nipkow [Mon, 12 Dec 2011 20:28:34 +0100] rev 45824
merged
2011-12-12 tuned
nipkow [Mon, 12 Dec 2011 20:28:19 +0100] rev 45823
tuned
2011-12-12 datatype dtyp with explicit sort information;
wenzelm [Mon, 12 Dec 2011 23:05:21 +0100] rev 45822
datatype dtyp with explicit sort information; tuned messages;
2011-12-12 tuned;
wenzelm [Mon, 12 Dec 2011 20:55:57 +0100] rev 45821
tuned;
2011-12-12 updated generated file;
wenzelm [Mon, 12 Dec 2011 19:47:50 +0100] rev 45820
updated generated file;
2011-12-12 tuned quickcheck's response
bulwahn [Mon, 12 Dec 2011 17:22:48 +0100] rev 45819
tuned quickcheck's response
2011-12-12 hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
bulwahn [Mon, 12 Dec 2011 13:45:54 +0100] rev 45818
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
2011-12-12 merged
huffman [Mon, 12 Dec 2011 12:03:34 +0100] rev 45817
merged
2011-12-12 replace more uses of 'lemmas' with explicit 'lemma';
huffman [Mon, 12 Dec 2011 08:19:37 +0100] rev 45816
replace more uses of 'lemmas' with explicit 'lemma'; replace uses of 'simplified' attribute with 'unfolded'; remove unused intermediate lemmas.
2011-12-12 Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Dec 2011 15:32:54 +0900] rev 45815
Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
2011-12-11 fix spelling
huffman [Sun, 11 Dec 2011 21:57:22 +0100] rev 45814
fix spelling
2011-12-11 fix spelling
huffman [Sun, 11 Dec 2011 21:54:20 +0100] rev 45813
fix spelling
2011-12-11 added IMP/Live_True.thy
nipkow [Sun, 11 Dec 2011 18:22:06 +0100] rev 45812
added IMP/Live_True.thy
2011-12-11 replace many uses of 'lemmas' with 'lemma';
huffman [Sun, 11 Dec 2011 09:55:57 +0100] rev 45811
replace many uses of 'lemmas' with 'lemma'; remove many unused intermediate lemmas.
2011-12-10 prove class instances without extra lemmas
huffman [Sat, 10 Dec 2011 22:00:42 +0100] rev 45810
prove class instances without extra lemmas
2011-12-10 finite class instance for word type; remove unused lemmas
huffman [Sat, 10 Dec 2011 21:48:16 +0100] rev 45809
finite class instance for word type; remove unused lemmas
2011-12-10 remove unused lemmas
huffman [Sat, 10 Dec 2011 21:07:59 +0100] rev 45808
remove unused lemmas
2011-12-10 generalize some lemmas
huffman [Sat, 10 Dec 2011 16:24:22 +0100] rev 45807
generalize some lemmas
2011-12-10 merged
huffman [Sat, 10 Dec 2011 13:00:58 +0100] rev 45806
merged
2011-12-10 tidied Word.thy;
huffman [Sat, 10 Dec 2011 08:29:19 +0100] rev 45805
tidied Word.thy; put attributes directly on lemmas instead of using 'declare'; replace various 'lemmas' commands with ordinary 'lemma'.
2011-12-09 remove redundant lemma word_diff_minus
huffman [Fri, 09 Dec 2011 14:52:51 +0100] rev 45804
remove redundant lemma word_diff_minus
2011-12-09 remove some duplicate lemmas, simplify some proofs
huffman [Fri, 09 Dec 2011 14:14:05 +0100] rev 45803
remove some duplicate lemmas, simplify some proofs
2011-12-09 Quotient_Info stores only relation maps
kuncar [Fri, 09 Dec 2011 18:07:04 +0100] rev 45802
Quotient_Info stores only relation maps
2011-12-09 hiding definitional facts in Quickcheck; introducing catch_match more honestly
bulwahn [Fri, 09 Dec 2011 16:08:32 +0100] rev 45801
hiding definitional facts in Quickcheck; introducing catch_match more honestly
2011-12-09 added dependencies
kuncar [Fri, 09 Dec 2011 14:46:18 +0100] rev 45800
added dependencies
2011-12-09 added an example file with lifting of constants with contravariant and co/contravariant types
kuncar [Fri, 09 Dec 2011 14:22:05 +0100] rev 45799
added an example file with lifting of constants with contravariant and co/contravariant types
2011-12-09 merged
kuncar [Fri, 09 Dec 2011 14:16:42 +0100] rev 45798
merged
2011-12-09 make ctxt the first parameter
kuncar [Fri, 09 Dec 2011 14:14:37 +0100] rev 45797
make ctxt the first parameter
2011-12-09 context/theory parametres tuned
kuncar [Fri, 09 Dec 2011 14:12:02 +0100] rev 45796
context/theory parametres tuned
2011-12-09 maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar [Fri, 09 Dec 2011 14:03:17 +0100] rev 45795
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
2011-12-09 add induction rule for list_all2
huffman [Fri, 09 Dec 2011 13:42:16 +0100] rev 45794
add induction rule for list_all2
2011-12-09 deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn [Fri, 09 Dec 2011 12:21:03 +0100] rev 45793
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
(0) -30000 -10000 -3000 -1000 -112 +112 +1000 +3000 +10000 +30000 tip