added at_set_avoiding lemmas

removed obsolete conversion guide -- converted only section on tactics;

converted ZF specific elements;

enabled ThyOutput.source option by default;

output_entity: ignore ThyOutput.source option;

updated generated file;

converted HOLCF specific elements;

added logic-specific sessions;

Updated.

Instantiated rule increasing_chain_adm_lemma in proof of flatstream_adm_lemma to avoid problems with HO unification.

Replaced instance declarations for sets by instance declarations for bool. Together with the instance declarations for fun from Ffun, this subsumes the old instance declarations for sets.

Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm, needs functions (since sets are now just functions).

Lookup and union operations on terms are now modulo eta conversion.

Terms returned by decomp are now eta-contracted.

Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.

eq_assumption now uses aeconv instead of aconv.

- Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv

Replaced Pattern.eta_contract_atom by Envir.eta_contract.

Removed instantiation for set.

Explicitely applied ext in proof of tnd.

Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.

- Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.

Manually applied subset_antisym in proof of Compl_fixedpoint, because it is accidentally applied to predicates as well.

Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped because of the new encoding of sets.

Functions get_branching_types and get_arities now use fold instead of foldl/r.

Temporarily disabled invocations of new code generator that do no longer work due to the encoding of sets as predicates

Replaced instance "set :: (plus) plus" by "fun :: (type, type) plus"

- Deleted arity proofs for set - Produce specific instances of theorems insert_eqvt, set_eqvt and perm_set_eq

Replaced union_empty2 by Un_empty_right.

Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that it gets applied to sets as well.

Deleted instance "set :: ({heap, finite}) heap"

- Declared subset_eq as code lemma - Deleted types_code declaration for sets

Deleted instantiation "set :: (enum) enum"

Replaced + and * on sets by \<oplus> and \<otimes>, to avoid clash with definitions of + and * on functions.

Rephrased calculational proofs to avoid problems with HO unification

Rephrased forward proofs to avoid problems with HO unification

Rephrased proof of ann_hoare_case_analysis, to avoid problems with HO unification

Locally deleted some definitions that were applied too eagerly because of eta-expansion

- Instantiated parts_insert_substD to avoid problems with HO unification - Replaced auto by fastsimp in proof of parts_invKey, since auto looped because of the new encoding of sets

Instantiated parts_insert_substD to avoid problems with HO unification

Replaced blast by fast in proof of parts_singleton, since blast looped because of the new encoding of sets.

Adapted to encoding of sets as predicates

Replaced forward proofs of existential statements by backward proofs to avoid problems with HO unification

Adapted functions mk_setT and dest_setT to encoding of sets as predicates.

- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set and to_pred attributes, because it is no longer applied automatically - Manually applied predicate1I in proof of accp_subset, because it is no longer part of the claset - Replaced psubset_def by less_le

Deleted instantiation "set :: (type) itself".

- Function dec in Trancl_Tac must eta-contract relation before calling decr, since it is now a function and could therefore be in eta-expanded form - The trancl prover now does more eta-contraction itself, so eta-contraction is no longer necessary in Tranclp_tac.

- Now uses Orderings as parent theory - "'a set" is now just a type abbreviation for "'a => bool" - The instantiation "set :: (type) ord" and the definition of (p)subset is no longer needed, since it is subsumed by the order on functions and booleans. The derived theorems (p)subset_eq can be used as a replacement. - mem_Collect_eq and Collect_mem_eq can now be derived from the definitions of mem and Collect. - Replaced the instantiation "set :: (type) minus" by the two instantiations "fun :: (type, minus) minus" and "bool :: minus". The theorem set_diff_eq can be used as a replacement for the definition set_diff_def - Replaced the instantiation "set :: (type) uminus" by the two instantiations "fun :: (type, uminus) uminus" and "bool :: uminus". The theorem Compl_eq can be used as a replacement for the definition Compl_def. - Variable P in rule split_if must be instantiated manually in proof of split_if_mem2 due to problems with HO unification - Moved definition of dense linear orders and proofs about LEAST from Orderings to Set - Deleted code setup for sets

Deleted instance "set :: (type) power" and moved instance "fun :: (type, type) power" to the beginning of the theory

split_beta is now declared as monotonicity rule, to allow bounded quantifiers in introduction rules of inductive predicates.

- Added mem_def and predicate1I in some of the proofs - pred_equals_eq and pred_subset_eq are no longer used in the conversion between sets and predicates, because sets and predicates can no longer be distinguished

- Now imports Code_Setup, rather than Set and Fun, since the theorems about orderings are already needed in Set - Moved "Dense orders" section to Set, since it requires set notation. - The "Order on sets" section is no longer necessary, since it is subsumed by the order on functions and booleans. - Moved proofs of Least_mono and Least_equality to Set, since they require set notation. - In proof of "instance fun :: (type, order) order", use ext instead of expand_fun_eq, since the latter is not yet available. - predicate1I is no longer declared as introduction rule, since it interferes with subsetI

- Explicitely applied predicate1I in a few proofs, because it is no longer part of the claset - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set attribute, because it is no longer applied automatically

- Now imports Fun rather than Orderings - Moved "Set as lattice" section behind "Fun as lattice" section, since sets are just functions. - The instantiations instantiation set :: (type) distrib_lattice instantiation set :: (type) complete_lattice are no longer needed, and the former definitions inf_set_eq, sup_set_eq, Inf_set_def, and Sup_set_def can now be derived from abstract properties of sup, inf, etc.

Instantiated some rules to avoid problems with HO unification.

- Deleted code setup for finite and card - Deleted proof of "instance set :: (finite) finite" and modified proof of "instance fun :: (finite, finite) finite", which now uses some ideas from the instance proof for sets - Instantiated arg_cong rule to avoid problems with HO unification

Instantiated subst rule to avoid problems with HO unification.

converted "General logic setup";

misc fixes and tuning;

updated generated file;

proper scoping of railaliases;

moved some railaliases here -- for proper scoping;

element: isakeyword markup;

removed isasymIN -- already defined in isar.sty;

added isasymIN/STRUCTURE;

converted generic.tex to Thy/Generic.thy;

removed isasymIMPORTS/BEGIN -- already defined in isar.sty;

tuned syntax: props and facts;

converted refcard.tex to Thy/Quick_Reference.thy;

added \isasymdash;

misc tuning;

updated generated file;

use underscore for underscore;

output_entity: added \mbox{} to prevent hyphenation;

added more infrastructure for fresh_star

added mising lemma

Added documentation

moved begin and imports to ../isar.sty;

added begin and imports;

clean_string: handle { };

converted pure.tex to Thy/pure.thy;

polished the proof for atm_prm_fresh and more lemmas for fresh_star

unfold_locales part of default method.

extended to be a library of general facts about the lambda calculus

tuned some proofs and comments

added lemma antiquotation

proper input abbreviations in class

replaced various macros by antiquotations; misc tuning;

more ref macros;

session based on HOL;

thms Max_ge, Min_le: dropped superfluous premise

proper command/keyword markup;

added AND, IS, WHERE symbols;

converted syntax.tex to Thy/syntax.thy;

dropping return in imperative monad bindings

corrected ML semantics

added setup for Isar entities; tuned;

fixed recdef, broken by my previous commit

* New attribute "termination_simp": Simp rules for termination proofs * General lemmas about list_size

Merged theories about wellfoundedness into one: Wellfounded.thy

moved 'trivial classes' to foundation of code generator

tuned index commands;

more abstract index commands;

added \indexoutersyntax; removed permuted index;

fixed proof

misc cleanup;

converted intro.tex to Thy/intro.thy;

more general evaluation combinators

different handling of eq class for nbe

basic setup for generated document (cf. ../IsarImplementation);

dropped theory PreList

added explicit check phase after reading of specification

added theory Sublist_Order

dropped some metis calls

tuned proofs

constant HOL.eq now qualified

exported is_abbrev mode discriminator

proper abbreviations in class

dropped theory PreList

added entries