wenzelm [Sat, 07 Oct 2006 01:31:10 +0200] rev 20882
added the_single;
wenzelm [Sat, 07 Oct 2006 01:31:09 +0200] rev 20881
added term_rule;
wenzelm [Sat, 07 Oct 2006 01:31:08 +0200] rev 20880
added Isar/theory_target.ML;
wenzelm [Sat, 07 Oct 2006 01:31:07 +0200] rev 20879
improved LocalDefs.add_def;
wenzelm [Sat, 07 Oct 2006 01:31:06 +0200] rev 20878
mk_partial_rules_mutual: expand result terms/thms;
wenzelm [Sat, 07 Oct 2006 01:31:05 +0200] rev 20877
removed with_local_path -- LocalTheory.note admits qualified names;
TheoryTarget.init;
wenzelm [Sat, 07 Oct 2006 01:31:04 +0200] rev 20876
moved the_single to Pure/library.ML;
tuned;
wenzelm [Sat, 07 Oct 2006 01:31:03 +0200] rev 20875
TheoryTarget.init;
wenzelm [Sat, 07 Oct 2006 01:31:02 +0200] rev 20874
tuned comments;
wenzelm [Sat, 07 Oct 2006 01:31:01 +0200] rev 20873
tuned method syntax: polymorhic term argument;
tuned rule instantiation;
wenzelm [Sat, 07 Oct 2006 01:30:58 +0200] rev 20872
tuned;
paulson [Fri, 06 Oct 2006 15:39:29 +0200] rev 20871
Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
Retains the ATP input files if debugging is on.
paulson [Fri, 06 Oct 2006 15:38:29 +0200] rev 20870
Tidied code to delete tmp files.
Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
paulson [Fri, 06 Oct 2006 11:17:53 +0200] rev 20869
renamed the combinator laws
paulson [Fri, 06 Oct 2006 11:17:27 +0200] rev 20868
Improved detection of identical clauses, also in the conjecture
paulson [Fri, 06 Oct 2006 11:16:40 +0200] rev 20867
Refinements to abstraction. Seeding with combinators K, I and B.
kleing [Fri, 06 Oct 2006 03:49:36 +0200] rev 20866
examples for hex and bin numerals
mengj [Thu, 05 Oct 2006 13:54:17 +0200] rev 20865
Changed and removed some functions related to combinators, since they are Isabelle constants now.
paulson [Thu, 05 Oct 2006 10:46:26 +0200] rev 20864
Now the DFG output includes correct declarations of c_fequal, but not hEXTENT
paulson [Thu, 05 Oct 2006 10:42:39 +0200] rev 20863
improvements to abstraction, ensuring more re-use of abstraction functions
moving some functions to Pure/drule.ML
paulson [Thu, 05 Oct 2006 10:41:27 +0200] rev 20862
facts about combinators
paulson [Thu, 05 Oct 2006 10:40:12 +0200] rev 20861
a few new functions on thms and cterms
huffman [Thu, 05 Oct 2006 05:46:32 +0200] rev 20860
reorganize and speed up termdiffs proofs
nipkow [Wed, 04 Oct 2006 18:41:14 +0200] rev 20859
fixed bug in linear arith
haftmann [Wed, 04 Oct 2006 15:10:44 +0200] rev 20858
improvements for Haskell serialization
haftmann [Wed, 04 Oct 2006 14:25:47 +0200] rev 20857
insert replacing ins ins_int ins_string
haftmann [Wed, 04 Oct 2006 14:17:47 +0200] rev 20856
cleaned up some mess
haftmann [Wed, 04 Oct 2006 14:17:46 +0200] rev 20855
clarified header comments
haftmann [Wed, 04 Oct 2006 14:17:38 +0200] rev 20854
insert replacing ins ins_int ins_string
haftmann [Wed, 04 Oct 2006 14:14:33 +0200] rev 20853
*** empty log message ***
webertj [Wed, 04 Oct 2006 11:50:37 +0200] rev 20852
tuned
krauss [Wed, 04 Oct 2006 11:18:39 +0200] rev 20851
Improved error reporting
webertj [Wed, 04 Oct 2006 01:43:57 +0200] rev 20850
nnf_simpset built statically
huffman [Tue, 03 Oct 2006 19:40:34 +0200] rev 20849
rewrite proofs of powser_insidea and termdiffs_aux
huffman [Mon, 02 Oct 2006 23:15:35 +0200] rev 20848
generalize summability lemmas using class banach
haftmann [Mon, 02 Oct 2006 23:01:14 +0200] rev 20847
clarified setup name
haftmann [Mon, 02 Oct 2006 23:01:11 +0200] rev 20846
various code refinements
haftmann [Mon, 02 Oct 2006 23:01:09 +0200] rev 20845
fixed some Haskell issues
haftmann [Mon, 02 Oct 2006 23:01:05 +0200] rev 20844
changed preprocessing framework
haftmann [Mon, 02 Oct 2006 23:01:04 +0200] rev 20843
clarified some things
haftmann [Mon, 02 Oct 2006 23:01:03 +0200] rev 20842
cleaned and extended
haftmann [Mon, 02 Oct 2006 23:01:00 +0200] rev 20841
added gen_primrec
haftmann [Mon, 02 Oct 2006 23:00:58 +0200] rev 20840
added code for insert
haftmann [Mon, 02 Oct 2006 23:00:57 +0200] rev 20839
improvements for code_gen
haftmann [Mon, 02 Oct 2006 23:00:56 +0200] rev 20838
cleaned mess
haftmann [Mon, 02 Oct 2006 23:00:53 +0200] rev 20837
added example for code_gen
haftmann [Mon, 02 Oct 2006 23:00:52 +0200] rev 20836
dropped obsolete Theory.sign_of
haftmann [Mon, 02 Oct 2006 23:00:51 +0200] rev 20835
tuned
haftmann [Mon, 02 Oct 2006 23:00:50 +0200] rev 20834
added code generator names for nat_rec and nat_case
haftmann [Mon, 02 Oct 2006 23:00:49 +0200] rev 20833
improved serialization for arbitrary
haftmann [Mon, 02 Oct 2006 23:00:46 +0200] rev 20832
normal_form now a diagnostic command
haftmann [Mon, 02 Oct 2006 23:00:45 +0200] rev 20831
restructured contents
huffman [Mon, 02 Oct 2006 21:30:05 +0200] rev 20830
add axclass banach for complete normed vector spaces
huffman [Mon, 02 Oct 2006 19:57:02 +0200] rev 20829
remove unused Cauchy_Bseq lemmas
huffman [Mon, 02 Oct 2006 18:30:10 +0200] rev 20828
add lemmas norm_not_less_zero, norm_le_zero_iff
paulson [Mon, 02 Oct 2006 17:33:13 +0200] rev 20827
added is_Trueprop
paulson [Mon, 02 Oct 2006 17:32:18 +0200] rev 20826
tidying and simplifying
paulson [Mon, 02 Oct 2006 17:32:03 +0200] rev 20825
Changing the default for theory_const
paulson [Mon, 02 Oct 2006 17:31:14 +0200] rev 20824
extensions for Susanto
paulson [Mon, 02 Oct 2006 17:30:56 +0200] rev 20823
restored the "length of name > 2" check for package definitions
paulson [Mon, 02 Oct 2006 17:29:42 +0200] rev 20822
Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
wenzelm [Sun, 01 Oct 2006 22:19:24 +0200] rev 20821
exists_name: include this theory name;
wenzelm [Sun, 01 Oct 2006 22:19:23 +0200] rev 20820
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm [Sun, 01 Oct 2006 22:19:21 +0200] rev 20819
merged with theory Datatype_Universe;
wenzelm [Sun, 01 Oct 2006 18:30:04 +0200] rev 20818
obsolete;
wenzelm [Sun, 01 Oct 2006 18:29:36 +0200] rev 20817
renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;
wenzelm [Sun, 01 Oct 2006 18:29:35 +0200] rev 20816
removed share_data;
tuned;
wenzelm [Sun, 01 Oct 2006 18:29:34 +0200] rev 20815
cterm_match: avoid recalculation of maxidx;
wenzelm [Sun, 01 Oct 2006 18:29:33 +0200] rev 20814
reverted to revision 1.28;
wenzelm [Sun, 01 Oct 2006 18:29:32 +0200] rev 20813
proper use of svc_oracle.ML;
wenzelm [Sun, 01 Oct 2006 18:29:31 +0200] rev 20812
reactivated theory PER;
removed obsolete StringEx;
wenzelm [Sun, 01 Oct 2006 18:29:30 +0200] rev 20811
tuned proofs;
wenzelm [Sun, 01 Oct 2006 18:29:28 +0200] rev 20810
moved theory Infinite_Set to Library;
tuned proofs;
wenzelm [Sun, 01 Oct 2006 18:29:26 +0200] rev 20809
moved theory Infinite_Set to Library;
wenzelm [Sun, 01 Oct 2006 18:29:25 +0200] rev 20808
moved Infinite_Set.thy to Library;
removed obsolete ex/StringEx.thy;
renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML;
wenzelm [Sun, 01 Oct 2006 18:29:23 +0200] rev 20807
tuned;
mengj [Sun, 01 Oct 2006 12:07:57 +0200] rev 20806
Removed the helper files (combinator rewrite rules, function extensionality and fequal rules).
huffman [Sun, 01 Oct 2006 03:07:12 +0200] rev 20805
generalize more DERIV proofs
wenzelm [Sat, 30 Sep 2006 21:39:31 +0200] rev 20804
statement: Variable.fix_frees;
wenzelm [Sat, 30 Sep 2006 21:39:29 +0200] rev 20803
added undo_end;
wenzelm [Sat, 30 Sep 2006 21:39:27 +0200] rev 20802
tuned proofs;
wenzelm [Sat, 30 Sep 2006 21:39:25 +0200] rev 20801
proper import of Main HOL;
wenzelm [Sat, 30 Sep 2006 21:39:24 +0200] rev 20800
tuned specifications and proofs;
wenzelm [Sat, 30 Sep 2006 21:39:22 +0200] rev 20799
hides popular names (from Datatype.thy);
wenzelm [Sat, 30 Sep 2006 21:39:20 +0200] rev 20798
removed obsolete sum_case_Inl/Inr;
moved 'hide' to Datatype_Universe;
tuned proofs;
wenzelm [Sat, 30 Sep 2006 21:39:17 +0200] rev 20797
renamed Variable.invent_fixes to Variable.variant_fixes;
huffman [Sat, 30 Sep 2006 20:54:34 +0200] rev 20796
generalize proofs of DERIV_isCont and DERIV_mult
huffman [Sat, 30 Sep 2006 19:41:06 +0200] rev 20795
generalized some DERIV proofs
huffman [Sat, 30 Sep 2006 18:04:28 +0200] rev 20794
add scaleR lemmas
huffman [Sat, 30 Sep 2006 17:36:55 +0200] rev 20793
generalize type of DERIV
huffman [Sat, 30 Sep 2006 17:10:55 +0200] rev 20792
add type annotations for DERIV
mengj [Sat, 30 Sep 2006 14:32:36 +0200] rev 20791
Combinator axioms are now from Isabelle theorems, no need to use helper files.
Removed LAM2COMB exception.
mengj [Sat, 30 Sep 2006 14:31:41 +0200] rev 20790
Added the combinator constants to the constants table.
mengj [Sat, 30 Sep 2006 14:31:02 +0200] rev 20789
Removed ResHolClause.LAM2COMB exception.
mengj [Sat, 30 Sep 2006 14:29:52 +0200] rev 20788
Reordered how files are loaded.
wenzelm [Fri, 29 Sep 2006 22:47:51 +0200] rev 20787
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm [Fri, 29 Sep 2006 22:47:04 +0200] rev 20786
removed mixfix_content;
wenzelm [Fri, 29 Sep 2006 22:47:03 +0200] rev 20785
Syntax.mode;
refrain from removing conflicting mixfixes;
wenzelm [Fri, 29 Sep 2006 22:47:01 +0200] rev 20784
Syntax.mode;
wenzelm [Fri, 29 Sep 2006 22:46:59 +0200] rev 20783
Sign.add_consts_authentic;
wenzelm [Fri, 29 Sep 2006 22:46:57 +0200] rev 20782
proper use of matrixlp.ML;
wenzelm [Fri, 29 Sep 2006 11:32:58 +0200] rev 20781
simplified is_package_def -- be less ambitious about B library operations;
wenzelm [Thu, 28 Sep 2006 23:43:02 +0200] rev 20780
obsolete;
wenzelm [Thu, 28 Sep 2006 23:43:00 +0200] rev 20779
added share_data;
wenzelm [Thu, 28 Sep 2006 23:42:59 +0200] rev 20778
Sign.add_consts_authentic;
wenzelm [Thu, 28 Sep 2006 23:42:56 +0200] rev 20777
consts: syntax consts only for actual syntax;
wenzelm [Thu, 28 Sep 2006 23:42:55 +0200] rev 20776
added share_data (dummy);
wenzelm [Thu, 28 Sep 2006 23:42:53 +0200] rev 20775
removed obsolete HOLCF.ML;
wenzelm [Thu, 28 Sep 2006 23:42:50 +0200] rev 20774
ResAtpset.get_atpset;
wenzelm [Thu, 28 Sep 2006 23:42:49 +0200] rev 20773
removed legacy code;
tuned;
wenzelm [Thu, 28 Sep 2006 23:42:47 +0200] rev 20772
tuned definitions/proofs;
wenzelm [Thu, 28 Sep 2006 23:42:45 +0200] rev 20771
proper use of float.ML;
wenzelm [Thu, 28 Sep 2006 23:42:43 +0200] rev 20770
fixed translations: CONST;
wenzelm [Thu, 28 Sep 2006 23:42:39 +0200] rev 20769
replaced syntax/translations by abbreviation;
fixed translations: CONST;
wenzelm [Thu, 28 Sep 2006 23:42:35 +0200] rev 20768
replaced syntax/translations by abbreviation;
wenzelm [Thu, 28 Sep 2006 23:42:32 +0200] rev 20767
removed obsolete Real/document/root.tex;
removed obsolete Isar_examples/Cantor.ML;
renamed Real/Float.ML to Real/float.ML;
wenzelm [Thu, 28 Sep 2006 23:42:30 +0200] rev 20766
tuned;
huffman [Thu, 28 Sep 2006 21:01:13 +0200] rev 20765
rearranged axioms and simp rules for scaleR
wenzelm [Thu, 28 Sep 2006 20:30:53 +0200] rev 20764
added Poly/ML 4.9.1 (experimental!);
huffman [Thu, 28 Sep 2006 19:04:13 +0200] rev 20763
rearranged axioms and simp rules for scaleR
paulson [Thu, 28 Sep 2006 16:01:48 +0200] rev 20762
clearout of obsolete code
paulson [Thu, 28 Sep 2006 16:01:34 +0200] rev 20761
addition of combinators
wenzelm [Thu, 28 Sep 2006 15:30:03 +0200] rev 20760
tuned messages;
wenzelm [Thu, 28 Sep 2006 11:56:30 +0200] rev 20759
tuned;
wenzelm [Thu, 28 Sep 2006 11:55:56 +0200] rev 20758
LD_LIBRARY_PATH;
paulson [Thu, 28 Sep 2006 11:04:41 +0200] rev 20757
Definitions produced by packages are now blacklisted.
huffman [Thu, 28 Sep 2006 06:21:06 +0200] rev 20756
more reorganizing sections
huffman [Thu, 28 Sep 2006 04:03:43 +0200] rev 20755
reorganize sections