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

- Added mem_def and predicate1I in some of the proofs
2008-05-07, by berghofe
- Now imports Code_Setup, rather than Set and Fun, since the theorems
2008-05-07, by berghofe
- Explicitely applied predicate1I in a few proofs, because it is no longer
2008-05-07, by berghofe
- Now imports Fun rather than Orderings
2008-05-07, by berghofe
Instantiated some rules to avoid problems with HO unification.
2008-05-07, by berghofe
- Deleted code setup for finite and card
2008-05-07, by berghofe
Instantiated subst rule to avoid problems with HO unification.
2008-05-07, by berghofe
converted "General logic setup";
2008-05-06, by wenzelm
misc fixes and tuning;
2008-05-06, by wenzelm
updated generated file;
2008-05-06, by wenzelm
proper scoping of railaliases;
2008-05-06, by wenzelm
moved some railaliases here -- for proper scoping;
2008-05-06, by wenzelm
element: isakeyword markup;
2008-05-06, by wenzelm
removed isasymIN -- already defined in isar.sty;
2008-05-05, by wenzelm
added isasymIN/STRUCTURE;
2008-05-05, by wenzelm
converted generic.tex to Thy/Generic.thy;
2008-05-05, by wenzelm
removed isasymIMPORTS/BEGIN -- already defined in isar.sty;
2008-05-04, by wenzelm
tuned syntax: props and facts;
2008-05-03, by wenzelm
converted refcard.tex to Thy/Quick_Reference.thy;
2008-05-03, by wenzelm
added \isasymdash;
2008-05-03, by wenzelm
misc tuning;
2008-05-02, by wenzelm
updated generated file;
2008-05-02, by wenzelm
use underscore for underscore;
2008-05-02, by wenzelm
output_entity: added \mbox{} to prevent hyphenation;
2008-05-02, by wenzelm
added more infrastructure for fresh_star
2008-05-02, by urbanc
added mising lemma
2008-05-02, by urbanc
Added documentation
2008-05-02, by nipkow
moved begin and imports to ../isar.sty;
2008-05-02, by wenzelm
added begin and imports;
2008-05-02, by wenzelm
clean_string: handle { };
2008-05-02, by wenzelm
converted pure.tex to Thy/pure.thy;
2008-05-02, by wenzelm
polished the proof for atm_prm_fresh and more lemmas for fresh_star
2008-05-02, by urbanc
unfold_locales part of default method.
2008-05-02, by ballarin
extended to be a library of general facts about the lambda calculus
2008-05-02, by urbanc
tuned some proofs and comments
2008-05-02, by urbanc
added lemma antiquotation
2008-04-29, by haftmann
proper input abbreviations in class
2008-04-29, by haftmann
replaced various macros by antiquotations;
2008-04-29, by wenzelm
more ref macros;
2008-04-29, by wenzelm
session based on HOL;
2008-04-29, by wenzelm
thms Max_ge, Min_le: dropped superfluous premise
2008-04-28, by haftmann
proper command/keyword markup;
2008-04-28, by wenzelm
added AND, IS, WHERE symbols;
2008-04-28, by wenzelm
converted syntax.tex to Thy/syntax.thy;
2008-04-28, by wenzelm
dropping return in imperative monad bindings
2008-04-28, by haftmann
corrected ML semantics
2008-04-27, by haftmann
added setup for Isar entities;
2008-04-26, by wenzelm
fixed recdef, broken by my previous commit
2008-04-26, by krauss
* New attribute "termination_simp": Simp rules for termination proofs
2008-04-25, by krauss
Merged theories about wellfoundedness into one: Wellfounded.thy
2008-04-25, by krauss
moved 'trivial classes' to foundation of code generator
2008-04-24, by haftmann
tuned index commands;
2008-04-24, by wenzelm
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
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