isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

tuned;
2007-06-04, by chaieb
monomorphic equality: let ML work out the details;
2007-06-03, by wenzelm
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
2007-06-03, by wenzelm
tuned Tactic signature;
2007-06-03, by wenzelm
removed obsolete Library.seq;
2007-06-03, by wenzelm
moved flip to library.ML;
2007-06-03, by wenzelm
added CSUBGOAL;
2007-06-03, by wenzelm
cleaned up signature;
2007-06-03, by wenzelm
added downto0 (from library.ML);
2007-06-03, by wenzelm
merge_ss: plain merge of prems;
2007-06-03, by wenzelm
added flip (from General/basics.ML);
2007-06-03, by wenzelm
tuned document;
2007-06-03, by wenzelm
use antiquotations instead of raw TeX code;
2007-06-03, by wenzelm
name_of_fqgar: precise type;
2007-06-03, by wenzelm
added plural (from Pure/library.ML);
2007-06-03, by wenzelm
local open FundefLib;
2007-06-03, by wenzelm
renamed gen_submultiset to submultiset;
2007-06-03, by wenzelm
HOL-ex: tuned deps;
2007-06-03, by wenzelm
tuned list comprehension, added lemma
2007-06-03, by nipkow
fixed tex error
2007-06-03, by nipkow
*** empty log message ***
2007-06-03, by nipkow
*** empty log message ***
2007-06-03, by nipkow
extended
2007-06-02, by webertj
cosmetic
2007-06-02, by webertj
made SML/NJ happy;
2007-06-02, by wenzelm
added target/local_abbrev (from proof_context.ML);
2007-06-02, by wenzelm
moved specific target/local_abbrev to theory_target.ML;
2007-06-02, by wenzelm
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
2007-06-02, by krauss
added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction
2007-06-02, by krauss
proper handling of Tools;
2007-06-02, by wenzelm
cosmetic
2007-06-02, by webertj
refute_tac made more deterministic
2007-06-02, by webertj
extended
2007-06-02, by webertj
cosmetic
2007-06-02, by webertj
tracing disabled
2007-06-02, by webertj
additional tracing information
2007-06-01, by webertj
tuned
2007-06-01, by webertj
some tests for arith added
2007-06-01, by webertj
Moved list comprehension into List
2007-06-01, by nipkow
MiniSAT mentioned in comment
2007-06-01, by webertj
fixed handling of meta-logic propositions
2007-06-01, by webertj
simplified interfaces, some restructuring
2007-06-01, by krauss
updated
2007-06-01, by krauss
added some bibtex entries
2007-06-01, by krauss
Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)
2007-06-01, by krauss
Added simp-rules: "R O {} = {}" and "{} O R = {}"
2007-06-01, by krauss
rudimenary
2007-06-01, by haftmann
tuned
2007-06-01, by haftmann
dropped superfluous name bindings
2007-06-01, by haftmann
localized
2007-06-01, by haftmann
fixed typo
2007-06-01, by haftmann
insert: canonical argument order;
2007-05-31, by wenzelm
simplified/unified list fold;
2007-05-31, by wenzelm
replace (- 1) with -1
2007-05-31, by huffman
simplify some proofs
2007-05-31, by huffman
tuned headers -- adapted to usual conventions;
2007-05-31, by wenzelm
moved Compute_Oracle from Pure/Tools to Tools;
2007-05-31, by wenzelm
proper theory setup for compute oracle (based on CPure);
2007-05-31, by wenzelm
moved IsaPlanner from Provers to Tools;
2007-05-31, by wenzelm
moved IsaPlanner from Provers to Tools;
2007-05-31, by wenzelm
made aconvc pervasive;
2007-05-31, by wenzelm
moved aconvc to more_thm.ML;
2007-05-31, by wenzelm
tuned ML setup;
2007-05-31, by wenzelm
decode_term: force qualified name into Const;
2007-05-31, by wenzelm
proper loading of ML files (in HOL.thy);
2007-05-31, by wenzelm
HOL_proofs;
2007-05-31, by wenzelm
moved Integ files to canonical place;
2007-05-31, by wenzelm
proper loading of ML files;
2007-05-31, by wenzelm
removed dead code;
2007-05-31, by wenzelm
tuned header;
2007-05-31, by wenzelm
doc: exclude isabelle_isar.pdf;
2007-05-31, by wenzelm
tuned the proof
2007-05-31, by urbanc
introduced symmetric variants of the lemmas for alpha-equivalence
2007-05-31, by urbanc
proper loading of ML files;
2007-05-31, by wenzelm
removed obsolete IFOL.thy/FOL.thy values;
2007-05-31, by wenzelm
proper loading of ML files;
2007-05-31, by wenzelm
tuned header;
2007-05-31, by wenzelm
tuned oracle setup;
2007-05-31, by wenzelm
moved HOLCF tools to canonical place;
2007-05-31, by wenzelm
moved TFL files to canonical place;
2007-05-31, by wenzelm
moved TFL files to canonical place;
2007-05-31, by wenzelm
added src/Tools;
2007-05-31, by wenzelm
fixed title;
2007-05-31, by wenzelm
Tools: generic tools outside of Pure.
2007-05-31, by wenzelm
moved Integ files to canonical place;
2007-05-31, by wenzelm
fixed use_thy "LocalWeakening";
2007-05-31, by wenzelm
included new example in the compiling process
2007-05-31, by urbanc
a theory using locally nameless terms and strong induction principles
2007-05-31, by urbanc
tuned the proof
2007-05-31, by urbanc
emulate later version of TextIO.inputLine;
2007-05-31, by wenzelm
reversed SML B library patches;
2007-05-31, by wenzelm
TextIO.inputLine: use present SML B library version;
2007-05-31, by wenzelm
tuned USEDIR_OPTIONS;
2007-05-30, by wenzelm
removed HOL4 image, which seldom works;
2007-05-30, by wenzelm
simplified data setup
2007-05-30, by haftmann
instance: always print sorts on failure
2007-05-30, by haftmann
more example
2007-05-30, by haftmann
fixed typo
2007-05-30, by haftmann
updated
2007-05-30, by haftmann
generalized lemmas
2007-05-30, by haftmann
eliminated strings
2007-05-30, by haftmann
tuned
2007-05-30, by haftmann
clarified error message
2007-05-30, by krauss
simplify names of locale interpretations
2007-05-30, by huffman
renamed some lemmas in Complex.thy
2007-05-30, by huffman
cleaned up proofs; reorganized sections; removed redundant lemmas
2007-05-30, by huffman
use new-style instance declarations
2007-05-29, by huffman
instance complex :: banach
2007-05-29, by huffman
add lemma real_sqrt_sum_squares_less
2007-05-29, by huffman
cleaned up some proofs
2007-05-29, by huffman
interpretation bounded_linear_divide
2007-05-29, by huffman
add bounded_linear lemmas
2007-05-29, by huffman
add isUCont lemmas
2007-05-29, by huffman
updated examples to include an instance of (lexicographic_order simp:...)
2007-05-29, by krauss
Complex: generalized type of exp
2007-05-28, by huffman
generalized exp to work over any complete field; new proof of exp_add
2007-05-28, by huffman
add type annotations for exp
2007-05-28, by huffman
interpretations additive_scaleR_left, additive_scaleR_right
2007-05-28, by huffman
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
2007-05-28, by huffman
new proof of Cauchy product formula for series
2007-05-27, by huffman