isabelle: Graph

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

prove_global: Variable.set_body true, pass context;
2008-04-17, by wenzelm
adapted to ProofContext.revert_skolem: extra Name.clean required;
2008-04-17, by wenzelm
prove_global: pass context;
2008-04-17, by wenzelm
pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
2008-04-17, by wenzelm
replaced token translations by common markup;
2008-04-17, by wenzelm
moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;
2008-04-17, by wenzelm
token translations: context dependent, result Pretty.T;
2008-04-17, by wenzelm
replaced token translations by common markup;
2008-04-17, by wenzelm
default token translations with proper markup;
2008-04-17, by wenzelm
token translations: context dependent, result Pretty.T;
2008-04-17, by wenzelm
removed obsolete raw_str;
2008-04-17, by wenzelm
added markup for fixed variables (local constants);
2008-04-17, by wenzelm
token translations: context dependent, result Pretty.T;
2008-04-17, by wenzelm
Pretty.mark;
2008-04-17, by wenzelm
unused_thms: sort_distinct;
2008-04-17, by wenzelm
Sign.add_path;
2008-04-16, by wenzelm
removed obsolete BASIC_THM_DEPS;
2008-04-16, by wenzelm
pretty_theorems: use proper PureThy.facts_of;
2008-04-16, by wenzelm
Facts.extern_static;
2008-04-16, by wenzelm
PureThy.defined_fact;
2008-04-16, by wenzelm
renamed check_fact to defined_fact;
2008-04-16, by wenzelm
removed unused space_of;
2008-04-16, by wenzelm
valid_facts: more elementary version using Facts.fold_static;
2008-04-16, by wenzelm
Facts.dest_static;
2008-04-16, by wenzelm
Auxiliary permutation functions are no longer declared using add_consts_i,
2008-04-16, by berghofe
removed unused TLA/Memory/MIParameters.thy;
2008-04-16, by wenzelm
removed obsolete valid_thms;
2008-04-16, by wenzelm
removed obsolete premsN;
2008-04-16, by wenzelm
PureThy.get_fact: pass dynamic context;
2008-04-16, by wenzelm
tuned;
2008-04-16, by wenzelm
removed obsolete get_fact_silent;
2008-04-16, by wenzelm
tuned proofs;
2008-04-16, by wenzelm
Added entry for unused_thms command.
2008-04-16, by berghofe
Adapted to new primrec package.
2008-04-16, by berghofe
Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).
2008-04-16, by berghofe
educated guess for infix syntax
2008-04-16, by haftmann
removed test artefacts
2008-04-16, by urbanc
proof endings: no Toplevel.print!
2008-04-15, by wenzelm
all_valid_thms: use new facts tables;
2008-04-15, by wenzelm
Theory.subthy;
2008-04-15, by wenzelm
Facts.intern, Facts.extern_table;
2008-04-15, by wenzelm
IsarCmd.hide_names;
2008-04-15, by wenzelm
added hide_names command (formerly Sign.hide_names), support fact name space;
2008-04-15, by wenzelm
Facts.dest_table, PureThy.facts_of;
2008-04-15, by wenzelm
simplified hide_XXX interfaces;
2008-04-15, by wenzelm
removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
2008-04-15, by wenzelm
removed obsolete SIGN_THEORY -- no name aliases in structure Theory;
2008-04-15, by wenzelm
added intern_fact, check_fact, hide_fact;
2008-04-15, by wenzelm
Theory.eq_thy;
2008-04-15, by wenzelm
renamed dest to dest_table, and extern to extern table;
2008-04-15, by wenzelm
PureThy.hide_fact;
2008-04-15, by wenzelm
Facts.dest_table;
2008-04-15, by wenzelm
Sign.hide_const;
2008-04-15, by wenzelm
added hide fact;
2008-04-15, by wenzelm
tuned;
2008-04-15, by wenzelm
removed eval_antiquotes_fn;
2008-04-15, by wenzelm
merge: canonical order;
2008-04-15, by wenzelm
Library.is_equal;
2008-04-15, by wenzelm
moved forall_elim_var(s) to more_thm.ML;
2008-04-15, by wenzelm
disallow duplicate entries (weak version for merge);
2008-04-15, by wenzelm
Thm.forall_elim_var(s);
2008-04-15, by wenzelm
proper dynamic facts for eqvts, freshs, bijs;
2008-04-15, by wenzelm
overloading perm: use big_name;
2008-04-15, by wenzelm
* Name space merge now observes canonical order;
2008-04-15, by wenzelm
removed redundant hd_append variant;
2008-04-14, by wenzelm
removed duplicate lemmas;
2008-04-14, by wenzelm
avoid duplicate fact bindings;
2008-04-14, by wenzelm
overloading of perm: adhoc name prevents duplicate fact names;
2008-04-14, by wenzelm
Changed naming scheme for theorems generated by interpretations.
2008-04-14, by ballarin
proper context for induct_scheme method
2008-04-14, by krauss
Isar.toplevel_loop: separate init/welcome flag;
2008-04-14, by wenzelm
Sorts.class_error: produce message only (formerly msg_class_error);
2008-04-13, by wenzelm
tsig: removed unnecessary universal witness;
2008-04-13, by wenzelm
simplified handling of sorts, removed unnecessary universal witness;
2008-04-13, by wenzelm
removed unused minimal_classes;
2008-04-13, by wenzelm
added insert_sorts (from thm.ML);
2008-04-13, by wenzelm
tsig: removed unnecessary universal witness;
2008-04-13, by wenzelm
tuned;
2008-04-13, by wenzelm
removed unnecessary Goal.close_result;
2008-04-12, by wenzelm
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12, by wenzelm
advance: do not count utf8 trailer bytes (which happen to be undefined or punctuation in iso-latin);
2008-04-12, by wenzelm
added is_utf8_trailer;
2008-04-12, by wenzelm
rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12, by wenzelm
obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;
2008-04-12, by wenzelm
removed obsolete compress.ML
2008-04-12, by wenzelm
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-12, by wenzelm
rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12, by wenzelm
rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-12, by wenzelm
use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;
2008-04-10, by wenzelm
transaction/init: ensure stable theory (non-draft);
2008-04-10, by wenzelm
export is_draft, not draftN;
2008-04-10, by wenzelm
simplified isarcmd;
2008-04-10, by wenzelm
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
2008-04-10, by wenzelm
eliminated unused trace, read;
2008-04-10, by wenzelm
eliminated unused Toplevel.print3/three_buffers;
2008-04-10, by wenzelm
tuned;
2008-04-10, by wenzelm
Isar.goal: tactical goal only;
2008-04-10, by wenzelm
eliminated backpatching of load_thy;
2008-04-10, by wenzelm
added read_const_exprs (from Pure/Isar/code_unit.ML);
2008-04-10, by wenzelm
export get_names (formerly names);
2008-04-10, by wenzelm
ThyInfo.get_names;
2008-04-10, by wenzelm
ThyInfo.get_theory;
2008-04-10, by wenzelm
export load_thy -- no backpatching;
2008-04-10, by wenzelm
export subst_alias;
2008-04-10, by wenzelm
load thy_info.ML after outer_syntax.ML -- avoids backpatching of load_thy;
2008-04-10, by wenzelm
val theory = ThyInfo.get_theory;
2008-04-10, by wenzelm
replaced Isar loop variants by generic toplevel_loop;
2008-04-10, by wenzelm
replaced Isar loop variants by generic toplevel_loop;
2008-04-10, by wenzelm
The global Isabelle/Isar state and main read-eval-print loop.
2008-04-10, by wenzelm
replaced Isar.toplevel by Toplevel.program;
2008-04-10, by wenzelm
moved global Toplevel state to structure Isar;
2008-04-10, by wenzelm
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
2008-04-10, by wenzelm