removed obsolete thumbpdf;

updated generated file;

use ../isabelle.sty, ../isabellesym.sty;

depend on ../pdfsetup.sty;

default linkcolor=black;

clean_name: replace "_" by "-";

updated generated file;

fixed some Isar element markups;

linkcolor=black (less noisy text);

hyperref is always enabled (also works with xdvi, dvips); replaced darkblue by generic linkcolor; reduced verbosity;

depend on ../pdfsetup.sty;

clean_string: cover <; added clean_name; output_entity: hyperlink;

updated generated file;

updated generated file;

proper checking of various Isar elements;

added defined_command, defined_option;

added intern, defined;

added defined;

setmp_thread_data: do nothing if Output.debugging;

names_of: exclude intermediate ids -- less verbosity;

remobed obsolete keyword concl;

explicit constraints for int literals;

use_text: added str_of_pos argument (ignored);

use_file: pass str_of_pos;

use_text/file: ignore str_of_pos argument;

use_text/file: proper position output;

renamed Position.path to Path.position; added line_file, ignore empty name;

renamed Position.path to Path.position;

load seq.ML and position.ML earlier;

adapted PolyML.compiler to latest change of basis/FinalPolyML.sml (2008-04-21);

fixed makefile

NEWS about measure functions

updated generated file;

Measure functions can now be declared via special rules, allowing for a prolog-style generation of measure functions for a specific type.

misc tuning;

updated generated file;

fixed some labels;

avoid old macros from isar.sty;

misc reorganization;

added chapters for "Specifications" and "Proofs";

removed outdated comment;

updated generated file;

proper antiquotations for commands;

removed obsolete macros for Isar commands etc.; tuned;

replaced macros by antiquotations;

removed obsolete macros for Isar commands etc.;

added local copy of underscore.sty;

updated generated file;

replaced some latex macros by antiquotations;

removed obsolete macros; tuned;

removed obsolete math macros;

depend on style.sty;

updated generated file;

depend on ../../antiquote_setup.ML;

improved treatment of "_" thanks to underscore.sty;

clean_string: map "_" to "\\_" (best used with underscore.sty);

misc tuning;

slight tuning of the 1st paragraph

unused;

converted HOL specific elements;

added rail setup for verblbrace, verbrbrace;

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

move some at/a64 tests to intel mac hardware (running Linux)

updated generated file;

updated generated file;

NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;

removed dead code;

print_cases: proper context for revert_skolem;

tuned;

modernized specifications and proofs;

improved definition of upd

* Context-dependent token translations.

revert_skolem: do not change non-reversible names; default token translations: revert_skolem; removed obsolete revert_skolems;

print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);

no_vars: reset body mode, i.e. invent global frees (which are acceptable to Variable.auto_fixes);

variant_fixes: preserve internal state, mark skolem only for body mode; import_inst: actually observe is_open flag (cf. variant_fixes);

prove_global: Variable.set_body true, pass context;

adapted to ProofContext.revert_skolem: extra Name.clean required;

prove_global: pass context;

pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);

replaced token translations by common markup; use XML.text instead of separate escape;

moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;

token translations: context dependent, result Pretty.T; added Markup.fixed (analogous to Markup.const); tuned;

replaced token translations by common markup;

default token translations with proper markup;

token translations: context dependent, result Pretty.T; string_of_term/prop: Variable.auto_fixes;

removed obsolete raw_str; added mark;

added markup for fixed variables (local constants);

token translations: context dependent, result Pretty.T;

Pretty.mark;

unused_thms: sort_distinct;

Sign.add_path;

removed obsolete BASIC_THM_DEPS; unused_thms: simplified signature, use proper PureThy.facts_of; misc tuning;

pretty_theorems: use proper PureThy.facts_of;

Facts.extern_static;

PureThy.defined_fact; unused_thms: simplified signature;

renamed check_fact to defined_fact;

removed unused space_of; added defined, fold_static; renamed dest_table to dest_static; renamed extern_table to extern_static;

valid_facts: more elementary version using Facts.fold_static;

Facts.dest_static;

Auxiliary permutation functions are no longer declared using add_consts_i, because add_primrec_overloaded can do this as well.

removed unused TLA/Memory/MIParameters.thy;

removed obsolete valid_thms; removed obsolete premsN binding; PureThy.get_fact: pass dynamic context;

removed obsolete premsN;

PureThy.get_fact: pass dynamic context;

tuned;

removed obsolete get_fact_silent; PureThy.get_fact: pass dynamic context; tuned;

tuned proofs;

Added entry for unused_thms command.

Adapted to new primrec package.

Added add_primrec_global and add_primrec_overloaded functions (thanks to Markus).

educated guess for infix syntax

removed test artefacts

proof endings: no Toplevel.print!

all_valid_thms: use new facts tables;

Theory.subthy;

Facts.intern, Facts.extern_table;

IsarCmd.hide_names;

added hide_names command (formerly Sign.hide_names), support fact name space;

Facts.dest_table, PureThy.facts_of;

simplified hide_XXX interfaces;