isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

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

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle