2008-04-24 wenzelm 2008-04-24 added \indexoutersyntax; removed permuted index;
2008-04-23 haftmann 2008-04-23 fixed proof
2008-04-23 wenzelm 2008-04-23 misc cleanup;
2008-04-23 wenzelm 2008-04-23 converted intro.tex to Thy/intro.thy;
2008-04-22 haftmann 2008-04-22 more general evaluation combinators
2008-04-22 haftmann 2008-04-22 different handling of eq class for nbe
2008-04-22 wenzelm 2008-04-22 basic setup for generated document (cf. ../IsarImplementation);
2008-04-22 haftmann 2008-04-22 dropped theory PreList
2008-04-22 haftmann 2008-04-22 added explicit check phase after reading of specification
2008-04-22 haftmann 2008-04-22 added theory Sublist_Order
2008-04-22 haftmann 2008-04-22 dropped some metis calls
2008-04-22 haftmann 2008-04-22 tuned proofs
2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified
2008-04-22 haftmann 2008-04-22 exported is_abbrev mode discriminator
2008-04-22 haftmann 2008-04-22 proper abbreviations in class
2008-04-22 haftmann 2008-04-22 dropped theory PreList
2008-04-22 haftmann 2008-04-22 added entries
2008-04-21 isatest 2008-04-21 move some at/a64 tests to intel mac hardware (running Linux)
2008-04-19 wenzelm 2008-04-19 updated generated file;
2008-04-19 wenzelm 2008-04-19 updated generated file;
2008-04-19 wenzelm 2008-04-19 NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
2008-04-18 wenzelm 2008-04-18 removed dead code;
2008-04-18 wenzelm 2008-04-18 print_cases: proper context for revert_skolem;
2008-04-18 wenzelm 2008-04-18 tuned;
2008-04-18 wenzelm 2008-04-18 modernized specifications and proofs;
2008-04-18 haftmann 2008-04-18 improved definition of upd
2008-04-17 wenzelm 2008-04-17 * Context-dependent token translations.
2008-04-17 wenzelm 2008-04-17 revert_skolem: do not change non-reversible names; default token translations: revert_skolem; removed obsolete revert_skolems;
2008-04-17 wenzelm 2008-04-17 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
2008-04-17 wenzelm 2008-04-17 no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);
2008-04-17 wenzelm 2008-04-17 variant_fixes: preserve internal state, mark skolem only for body mode; import_inst: actually observe is_open flag (cf. variant_fixes);
2008-04-17 wenzelm 2008-04-17 prove_global: Variable.set_body true, pass context;
2008-04-17 wenzelm 2008-04-17 adapted to ProofContext.revert_skolem: extra Name.clean required;
2008-04-17 wenzelm 2008-04-17 prove_global: pass context;
2008-04-17 wenzelm 2008-04-17 pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
2008-04-17 wenzelm 2008-04-17 replaced token translations by common markup; use XML.text instead of separate escape;
2008-04-17 wenzelm 2008-04-17 moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;
2008-04-17 wenzelm 2008-04-17 token translations: context dependent, result Pretty.T; added Markup.fixed (analogous to Markup.const); tuned;
2008-04-17 wenzelm 2008-04-17 replaced token translations by common markup;
2008-04-17 wenzelm 2008-04-17 default token translations with proper markup;
2008-04-17 wenzelm 2008-04-17 token translations: context dependent, result Pretty.T; string_of_term/prop: Variable.auto_fixes;
2008-04-17 wenzelm 2008-04-17 removed obsolete raw_str; added mark;
2008-04-17 wenzelm 2008-04-17 added markup for fixed variables (local constants);
2008-04-17 wenzelm 2008-04-17 token translations: context dependent, result Pretty.T;
2008-04-17 wenzelm 2008-04-17 Pretty.mark;
2008-04-17 wenzelm 2008-04-17 unused_thms: sort_distinct;
2008-04-16 wenzelm 2008-04-16 Sign.add_path;
2008-04-16 wenzelm 2008-04-16 removed obsolete BASIC_THM_DEPS; unused_thms: simplified signature, use proper PureThy.facts_of; misc tuning;
2008-04-16 wenzelm 2008-04-16 pretty_theorems: use proper PureThy.facts_of;
2008-04-16 wenzelm 2008-04-16 Facts.extern_static;
2008-04-16 wenzelm 2008-04-16 PureThy.defined_fact; unused_thms: simplified signature;
2008-04-16 wenzelm 2008-04-16 renamed check_fact to defined_fact;
2008-04-16 wenzelm 2008-04-16 removed unused space_of; added defined, fold_static; renamed dest_table to dest_static; renamed extern_table to extern_static;
2008-04-16 wenzelm 2008-04-16 valid_facts: more elementary version using Facts.fold_static;
2008-04-16 wenzelm 2008-04-16 Facts.dest_static;
2008-04-16 berghofe 2008-04-16 Auxiliary permutation functions are no longer declared using add_consts_i, because add_primrec_overloaded can do this as well.
2008-04-16 wenzelm 2008-04-16 removed unused TLA/Memory/MIParameters.thy;
2008-04-16 wenzelm 2008-04-16 removed obsolete valid_thms; removed obsolete premsN binding; PureThy.get_fact: pass dynamic context;
2008-04-16 wenzelm 2008-04-16 removed obsolete premsN;
2008-04-16 wenzelm 2008-04-16 PureThy.get_fact: pass dynamic context;