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

Removal of the "keep_types" flag: we always keep types!
2006-12-12, by paulson
make SML/NJ happy;
2006-12-12, by wenzelm
made SML/NJ happy;
2006-12-12, by wenzelm
consistent naming for FreeUltrafilterNat lemmas; cleaned up
2006-12-12, by huffman
cleaned up; generalized some proofs
2006-12-12, by huffman
fix assumptions on NSDERIV_quotient
2006-12-12, by huffman
changed (ns)deriv to take functions of type 'a::real_normed_field => 'a
2006-12-12, by huffman
generalize some theorems
2006-12-12, by huffman
add type annotation
2006-12-12, by huffman
read_xnum: return leading_zeros, radix;
2006-12-12, by wenzelm
authentic syntax for Pls/Min/Bit;
2006-12-12, by wenzelm
authentic syntax for Pls/Min/Bit;
2006-12-12, by wenzelm
binary numerals: restricted to actual abstract syntax;
2006-12-12, by wenzelm
Hyperreal/FrechetDeriv.thy
2006-12-12, by huffman
theory of Frechet derivatives
2006-12-12, by huffman
specials: include single quote;
2006-12-11, by wenzelm
xstr: disallow backslashes;
2006-12-11, by wenzelm
advanced translation functions: Proof.context;
2006-12-11, by wenzelm
advanced translation functions: Proof.context;
2006-12-11, by wenzelm
added improved versions of use_text/file (still inactive);
2006-12-11, by wenzelm
added use_file;
2006-12-11, by wenzelm
load secure.ML after symbol.ML, when default output is active;
2006-12-11, by wenzelm
ordered lists instead of tables for resolving hyps; speedup
2006-12-11, by webertj
nominal_primrec now prints initial proof state.
2006-12-11, by berghofe
Abbreviations can now be specified simultaneously
2006-12-11, by berghofe
Adapted to new inductive definition package.
2006-12-11, by berghofe
added ProofGeneral settings;
2006-12-11, by wenzelm
tuned comments;
2006-12-10, by wenzelm
tuned;
2006-12-10, by wenzelm
defs: increased entropy of mixfix handling;
2006-12-10, by wenzelm
fixed term_of_list;
2006-12-10, by wenzelm
Concrete syntax for hex chars and strings.
2006-12-10, by wenzelm
renamed str_of_XXX to print_XXX;
2006-12-10, by wenzelm
HOLogic cleanup;
2006-12-10, by wenzelm
ML_Syntax.print_XXX;
2006-12-10, by wenzelm
misc cleanup -- removed non-HOL operations;
2006-12-10, by wenzelm
moved char/string syntax to Tools/string_syntax.ML;
2006-12-10, by wenzelm
added Tools/string_syntax.ML;
2006-12-10, by wenzelm
removed junk;
2006-12-10, by wenzelm
interpretation: use C_class name prefix;
2006-12-10, by wenzelm
abs/binder_tr': support printing of idtdummy;
2006-12-10, by wenzelm
respects2: tuned spacing;
2006-12-10, by wenzelm
support printing of idtdummy;
2006-12-10, by wenzelm
added is_class (approximation);
2006-12-10, by wenzelm
LocalTheory.notation/abbrev;
2006-12-10, by wenzelm
extract_case: Name.clean;
2006-12-10, by wenzelm
added target_notation/abbrev;
2006-12-10, by wenzelm
added notation/abbrev (from term_syntax.ML);
2006-12-10, by wenzelm
tuned absdummy;
2006-12-10, by wenzelm
added no_frees;
2006-12-10, by wenzelm
removed (cf. proof_context.ML and local_theory.ML);
2006-12-10, by wenzelm
removed Isar/term_syntax.ML;
2006-12-10, by wenzelm
avoid internal name O_;
2006-12-10, by wenzelm
hide const linorder.less_eq_less.max linorder.less_eq_less.min;
2006-12-10, by wenzelm
hardwired option -q;
2006-12-10, by wenzelm
added print_abbrevs;
2006-12-10, by wenzelm
renaming
2006-12-10, by nipkow
Modified lattice locale
2006-12-10, by nipkow
updated;
2006-12-09, by wenzelm
added internal_mode;
2006-12-09, by wenzelm
simplified abbrev: single argument;
2006-12-09, by wenzelm
TermSyntax.abbrev;
2006-12-09, by wenzelm
added read/pretty_term_abbrev, print_abbrevs;
2006-12-09, by wenzelm
init_context: reset naming;
2006-12-09, by wenzelm
added 'print_abbrevs';
2006-12-09, by wenzelm
added print_abbrevs;
2006-12-09, by wenzelm
added term_abbrev;
2006-12-09, by wenzelm
renamed reserved to reserved_names;
2006-12-09, by wenzelm
tuned Consts signature;
2006-12-09, by wenzelm
abbrevs: print original rhs;
2006-12-09, by wenzelm
abbreviate: always authentic, force expansion of internal abbreviations;
2006-12-09, by wenzelm
ML_Syntax.reserved(_names);
2006-12-09, by wenzelm
TermSyntax.abbrev;
2006-12-09, by wenzelm
added antiquotation abbrev;
2006-12-09, by wenzelm
added print_abbrevs;
2006-12-09, by wenzelm
tuned use_text;
2006-12-08, by wenzelm
added 'help' command (same of 'print_commands');
2006-12-08, by wenzelm
more careful evaluation of ML text, prevents spurious output;
2006-12-08, by wenzelm
date: forcing LC_ALL=C prevents funny file names;
2006-12-08, by wenzelm
root function: restore default interrupt handler;
2006-12-08, by wenzelm
patched up the proofs agsin
2006-12-08, by paulson
removed use of put_name_hint, as the ATP linkup no longer needs this
2006-12-08, by paulson
reorganized structure Tactic vs. MetaSimplifier;
2006-12-07, by wenzelm
begin/end blocks;
2006-12-07, by wenzelm
abbrevs: more careful interpretation, avoid dynamic references to local names;
2006-12-07, by wenzelm
definition/abbreviation: single argument;
2006-12-07, by wenzelm
simplified add_abbrev -- single argument;
2006-12-07, by wenzelm
removed obsolete references to ProofGeneral/isa;
2006-12-07, by wenzelm
added input_mode;
2006-12-07, by wenzelm
tuned print_locale output;
2006-12-07, by wenzelm
moved notation/abbrevs to TermSyntax;
2006-12-07, by wenzelm
expand_term: based on Envir.expand_term;
2006-12-07, by wenzelm
thms etc.: proper treatment of internal_fact with selection;
2006-12-07, by wenzelm
tuned pretty_src output;
2006-12-07, by wenzelm
simplified add_abbrevs: no mixfix;
2006-12-07, by wenzelm
added expand_term;
2006-12-07, by wenzelm
tuned;
2006-12-07, by wenzelm
Common term syntax declarations.
2006-12-07, by wenzelm
added Isar/term_syntax.ML;
2006-12-07, by wenzelm
TermSyntax.notation/abbrevs;
2006-12-07, by wenzelm
Removal of theorem tagging, which the ATP linkup no longer requires.
2006-12-07, by paulson
Removal of theorem tagging, which the ATP linkup no longer requires,
2006-12-07, by paulson
Poly/ML 5.0 setup for Isabelle2005.
2006-12-07, by wenzelm
reorganized structure Goal vs. Tactic;
2006-12-07, by wenzelm
export: added explicit term operation;
2006-12-06, by wenzelm
abbrevs: actually observe target_morphism;
2006-12-06, by wenzelm
added expand;
2006-12-06, by wenzelm
moved hidden_polymorphism to term.ML;
2006-12-06, by wenzelm
added hidden_polymorphism (from variable.ML);
2006-12-06, by wenzelm
add_abbrevs: moved common parts to consts.ML;
2006-12-06, by wenzelm
abbreviate: improved error handling, return result;
2006-12-06, by wenzelm
export: added explicit term operation;
2006-12-06, by wenzelm
LocalDefs.expand;
2006-12-06, by wenzelm
Improved tracing
2006-12-06, by paulson
no timing;
2006-12-06, by wenzelm
simplified ML bindings;
2006-12-06, by wenzelm
simplified ML bindings -- moved to HOL.thy;
2006-12-06, by wenzelm
added basic ML bindings;
2006-12-06, by wenzelm
added aliases for nat_recs/cases;
2006-12-06, by wenzelm
removed legacy ML bindings;
2006-12-06, by wenzelm