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

updated to E 0.999-006;
2008-05-31, by wenzelm
THIS_IS_ISABELLE_MAKEBIN is back;
2008-05-30, by wenzelm
cvs2cl only for unofficial releases;
2008-05-30, by wenzelm
more AFP sessions;
2008-05-30, by wenzelm
*** empty log message ***
2008-05-30, by nipkow
Updated function tutorial.
2008-05-30, by krauss
(adjusted)
2008-05-30, by haftmann
various code streamlining
2008-05-30, by haftmann
more AFP sessions;
2008-05-30, by wenzelm
legacy_feature: no proof context in simpset;
2008-05-29, by wenzelm
proper context for attribute simplified;
2008-05-29, by wenzelm
added warning_count for issued reconstruction failure messages (limit 10);
2008-05-29, by wenzelm
proper context for ss;
2008-05-29, by wenzelm
proper context for simp_thms_conv;
2008-05-29, by wenzelm
added warning_count for issued reconstruction failure messages;
2008-05-29, by wenzelm
tuned;
2008-05-29, by wenzelm
*** empty log message ***
2008-05-29, by nipkow
yet another attempt to circumvent printmode problems
2008-05-29, by haftmann
obsolete;
2008-05-28, by wenzelm
moved README-polyml to polyml/README;
2008-05-28, by wenzelm
README for Poly/ML 5.2 distribution;
2008-05-28, by wenzelm
tuned;
2008-05-28, by wenzelm
more contribs;
2008-05-28, by wenzelm
misc tuning for Isabelle2008;
2008-05-28, by wenzelm
added some notable improvements;
2008-05-28, by wenzelm
tuned version numbers;
2008-05-28, by wenzelm
prepared for Isabelle2008;
2008-05-28, by wenzelm
added ISABELLE_HOME to startup;
2008-05-28, by wenzelm
added Substring.full;
2008-05-28, by wenzelm
moved distinctness_limit to datatype_rep_proofs.ML
2008-05-28, by haftmann
fixed utterly wrong print mode handling
2008-05-28, by haftmann
new serializer interface
2008-05-28, by haftmann
added new code_datatype example
2008-05-28, by haftmann
proper use of the Pretty module
2008-05-26, by haftmann
permissive wrt. instantiation of class operations
2008-05-26, by haftmann
proper lemma [source] antiquotation
2008-05-26, by haftmann
check for illegal merge of class parameters
2008-05-26, by haftmann
proper NoSubsort CLASS_ERROR
2008-05-26, by haftmann
tuned theorem order
2008-05-26, by haftmann
inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
2008-05-24, by wenzelm
updated generated file;
2008-05-24, by wenzelm
added local_theory command wrappers;
2008-05-24, by wenzelm
uniform treatment of target, not as config;
2008-05-24, by wenzelm
more uniform treatment of OuterSyntax.local_theory commands;
2008-05-24, by wenzelm
updated generated file;
2008-05-24, by wenzelm
invisible comment;
2008-05-24, by wenzelm
function: uniform treatment of target, not as config;
2008-05-24, by wenzelm
added parse_document (optional unchecked header material);
2008-05-24, by wenzelm
exported master_directory;
2008-05-24, by wenzelm
present_excursion: setmp_thread_position during presentation;
2008-05-24, by wenzelm
use: explicit .ML;
2008-05-24, by wenzelm
ident: naive caching prevents potentially slow external invocations;
2008-05-24, by wenzelm
fixed improper handling of return code (pdf and ps.gz formats)
2008-05-24, by urbanc
add constants: set Markup.theory_nameN in tags;
2008-05-23, by wenzelm
added theory_nameN;
2008-05-23, by wenzelm
rearranged subsections
2008-05-23, by krauss
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
2008-05-23, by berghofe
Replaced Pretty.str and Pretty.string_of by specific functions that
2008-05-23, by berghofe
temporary adjustment
2008-05-23, by haftmann
tuned
2008-05-23, by haftmann
more permissive preprocessor
2008-05-23, by haftmann
explicit type schemes for functions
2008-05-23, by haftmann
moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
2008-05-23, by haftmann
added code for quantifiers
2008-05-23, by haftmann
simplified proof
2008-05-23, by haftmann
made the naming of the induction principles consistent: weak_induct is
2008-05-22, by urbanc
use_file: added str_of_pos argument (ignored);
2008-05-21, by gagern
Added entry explaining incompatibilities introduced by replacing sets by predicates.
2008-05-21, by berghofe
instantiation lift :: (countable) bifinite
2008-05-19, by huffman
use new class package for classes profinite, bifinite; remove approx class
2008-05-19, by huffman
updated generated file;
2008-05-18, by wenzelm
unparse_term: check PureThy.old_appl_syntax instead of CPure;
2008-05-18, by wenzelm
theory Pure provides regular application syntax by default;
2008-05-18, by wenzelm
converted to regular application syntax;
2008-05-18, by wenzelm
eliminated theory CPure;
2008-05-18, by wenzelm
setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
2008-05-18, by wenzelm
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
2008-05-18, by wenzelm
proper handling of the return code for the ps-format (fixes a bug)
2008-05-18, by urbanc
oops -- pr_graph = Syntax.string_of_term;
2008-05-18, by wenzelm
command 'normal_form': proper context via Variable.auto_fixes;
2008-05-18, by wenzelm
moved global pretty/string_of functions from Sign to Syntax;
2008-05-18, by wenzelm
Syntax.string_of_sort: proper context;
2008-05-18, by wenzelm
pprint: proper global context via Syntax.init_pretty_global;
2008-05-18, by wenzelm
Syntax.string_of_typ: proper context;
2008-05-18, by wenzelm
moved global pretty/string_of functions from Sign to Syntax;
2008-05-18, by wenzelm
removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
2008-05-18, by wenzelm
renamed type decompT to decomp;
2008-05-18, by wenzelm
Syntax.string_of_term with proper context;
2008-05-18, by wenzelm
moved global pretty/string_of functions from Sign to Syntax;
2008-05-18, by wenzelm
renamed type decompT to decomp;
2008-05-18, by wenzelm
pr_matrix: proper context;
2008-05-18, by wenzelm
guess_instance: proper context;
2008-05-18, by wenzelm
moved global pretty/string_of functions from Sign to Syntax;
2008-05-18, by wenzelm
tuned comments;
2008-05-17, by wenzelm
tuned proofs;
2008-05-17, by wenzelm
avoid undeclared variables in facts;
2008-05-17, by wenzelm
avoid undeclared variables within proofs;
2008-05-17, by wenzelm
avoid undeclared variables within proofs;
2008-05-17, by wenzelm
tuned proof;
2008-05-17, by wenzelm
avoid undeclared variables within proofs;
2008-05-17, by wenzelm
cat_lines;
2008-05-17, by wenzelm
default token translations: observe Sign.is_pretty_global for fixed variables;
2008-05-17, by wenzelm
added pretty_global flag;
2008-05-17, by wenzelm
structure Display: less pervasive operations;
2008-05-17, by wenzelm
rename locales;
2008-05-16, by huffman
added a lemma about existence of contexts
2008-05-16, by urbanc
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
2008-05-16, by wenzelm
removed obsolete option open;
2008-05-16, by wenzelm
removed unused make_simple;
2008-05-16, by wenzelm
removed obsolete case rule_context;
2008-05-16, by wenzelm
fix looping simplifier
2008-05-16, by huffman
tuned;
2008-05-15, by wenzelm
tuned comment;
2008-05-15, by wenzelm
updated version;
2008-05-15, by wenzelm
removed unnecessary/untrusive a4paper option;
2008-05-15, by wenzelm
use Isabelle sty files from Doc/;
2008-05-15, by wenzelm
removed obsolete \ifpdfoutput;
2008-05-15, by wenzelm
* Simplified pdfsetup.sty;
2008-05-15, by wenzelm
use Isabelle sty files from Doc/;
2008-05-15, by wenzelm
updated generated file;
2008-05-15, by wenzelm