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

more abstract index commands;
2008-04-24, by wenzelm
added \indexoutersyntax;
2008-04-24, by wenzelm
fixed proof
2008-04-23, by haftmann
misc cleanup;
2008-04-23, by wenzelm
converted intro.tex to Thy/intro.thy;
2008-04-23, by wenzelm
more general evaluation combinators
2008-04-22, by haftmann
different handling of eq class for nbe
2008-04-22, by haftmann
basic setup for generated document (cf. ../IsarImplementation);
2008-04-22, by wenzelm
dropped theory PreList
2008-04-22, by haftmann
added explicit check phase after reading of specification
2008-04-22, by haftmann
added theory Sublist_Order
2008-04-22, by haftmann
dropped some metis calls
2008-04-22, by haftmann
tuned proofs
2008-04-22, by haftmann
constant HOL.eq now qualified
2008-04-22, by haftmann
exported is_abbrev mode discriminator
2008-04-22, by haftmann
proper abbreviations in class
2008-04-22, by haftmann
dropped theory PreList
2008-04-22, by haftmann
added entries
2008-04-22, by haftmann
move some at/a64 tests to intel mac hardware (running Linux)
2008-04-21, by isatest
updated generated file;
2008-04-19, by wenzelm
updated generated file;
2008-04-19, by wenzelm
NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
2008-04-19, by wenzelm
removed dead code;
2008-04-18, by wenzelm
print_cases: proper context for revert_skolem;
2008-04-18, by wenzelm
tuned;
2008-04-18, by wenzelm
modernized specifications and proofs;
2008-04-18, by wenzelm
improved definition of upd
2008-04-18, by haftmann
* Context-dependent token translations.
2008-04-17, by wenzelm
revert_skolem: do not change non-reversible names;
2008-04-17, by wenzelm
print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
2008-04-17, by wenzelm
no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);
2008-04-17, by wenzelm
variant_fixes: preserve internal state, mark skolem only for body mode;
2008-04-17, by wenzelm
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

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

isabelle