now uses -m symbols;

split ast_of_term(T); ast_of_term now marks frees; added token translation support;

added token translation support;

term_of_... now mark class, tfree, tvar;

added mark_bound(T), variant_abs'; trfuns now mark bounds they introduce!! added pure_trfunsT;

Token translations for xterm and LaTeX output.

added _mk_ofclass(S);

added strlen (includes metric information); removed map_strs;

added token_translation interface;

added add_tokentrfuns;

added Syntax/token_trans.ML;

added token_trans.ML;

Slightly more robust proof

dup_intr & dup_elim no longer call standard -- this lets them be used on meta-hyps

rule_by_tactic no longer standardizes its result

Addition of de Bruijn formulae

tuned comment;

tuned comments;

added proper subset symbols syntax;

minor changes due to primrec defintions for +,-,*

minor changes due to new primrec definitions for +,-,*

definitions of +,-,* replaced by primrec definitions

function nat_add_primrec added to allow primrec definitions over nat

removed explicit_domains/, which is now covered by ex/

added "_" syntax for dummyT;

declared the dummy type;

replaced natural by subset;

tuned symbolic [|_|] syntax;

tuned some chars;

More robust proof (?)

Replaced "flat" by the Basis Library function List.concat

Introduction of rotate_rule

removed empty line (which broke xfedor);

don't hack, use xfed or xfedor;

fixed Id comment;

makedist -- make Isabelle distribution.

tuned URL;

added index info;

index info;

added dist;

some administrative tools for the Isabelle;

made a bit more robust for 'make dist';

rail output;

fixed rail.sty dep;

added this file;

rail output;

made a bit more robust;

manual steps comment;

*** empty log message ***

described changes for HOLCF-Version without rules and arities

file moved;

file moved here;

configure - adapt Isabelle distribution to system environment

improved description of recent changes

reflecting recent changes of the simplifier

corrected type of plift

reflecting recent changes of the simplifier

mk_rews: automatically includes strip_shyps, zero_var_indexes;

New file for theorems of Porder0 Dervie the prperties of partial orders from the axiomatic type class po

tuned comments;

Examples are adopted to the changes from HOLCF. Classlib is reduced. Classlib still uses arities, Classlib will change completely to new classes of ADTs

using types one = unit lift and translations causes troubles between the type one and the constant one. The later was changed to ONE

Changes of HOLCF from Oscar Slotosch: 1. axclass instead of class * less instead of less_fun, less_cfun, less_sprod, less_cprod, less_ssum, less_up, less_lift * @x.!y.x<<y instead of UUU instead of UU_fun, UU_cfun, ... * no witness type void needed (eliminated Void.thy.Void.ML) * inst_<typ>_<class> derived as theorems 2. improved some proves on less_sprod and less_cprod * eliminated the following theorems Sprod1.ML: less_sprod1a Sprod1.ML: less_sprod1b Sprod1.ML: less_sprod2a Sprod1.ML: less_sprod2b Sprod1.ML: less_sprod2c Sprod2.ML: less_sprod3a Sprod2.ML: less_sprod3b Sprod2.ML: less_sprod4b Sprod2.ML: less_sprod4c Sprod3.ML: less_sprod5b Sprod3.ML: less_sprod5c Cprod1.ML: less_cprod1b Cprod1.ML: less_cprod2a Cprod1.ML: less_cprod2b Cprod1.ML: less_cprod2c Cprod2.ML: less_cprod3a Cprod2.ML: less_cprod3b 3. new classes: * cpo<po, * chfin<pcpo, * flat<pcpo, * derived: flat<chfin to do: show instances for lift 4. Data Type One * Used lift for the definition: one = unit lift * Changed the constant one into ONE 5. Data Type Tr * Used lift for the definition: tr = bool lift * adopted definitions of if,andalso,orelse,neg * only one theory Tr.thy,Tr.ML instead of Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML * reintroduced ceils for =TT,=FF 6. typedef * Using typedef instead of faking type definitions to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun 7. adopted examples and domain construct to theses changes These changes eliminated all rules and arities from HOLCF

*** empty log message ***

reflecting my recent changes of the classical reasoner

reflecting my recent changes of the simplifier and classical reasoner

added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss, safe_asm_more_full_simp_ta, clasimpset HOL_css with modification functions new addss (old version retained as unsafe_addss), new Addss (old version retained as Unsafe_Addss), new auto_tac (old version retained as unsafe_auto_tac),

cosmetic

updated mini_ss

added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss, safe_asm_more_full_simp_tac new addss (old version retained as unsafe_addss), new auto_tac (old version retained as unsafe_auto_tac), clasimpset with modification functions

corrected minor mistakes

description of safe vs. unsafe wrapper and the functions involved

moved THEN_MAYBE to Pure/tctical.ML better addbefore, addafter (now: addaltern), setwrapper (now: setWrapper) and addwrapper (now addWrapper) added safe wrapper(and functions setSWrapper,compSWrapper,addSbefore,addSaltern)

added deleqcongs, richer rep_ss split solver in safe and unsafe parts (finish_tac, unsafe_finish_tac) added safe_asm_full_simp_tac, setSSolver, addSSolver renamed setsolver to setSolver, addsolver to addSolver

description of del(eq)congs, safe and unsafe solver

added THEN_MAYBE and THEN_MAYBE'

added del_congs

Some lemmas changed to valuesd

fixed comment;

improved interface options;

semi fix of piping-quit peoblem (should work on systems with *real* sh);

globally unset ENV, BASH_ENV;

Made troublesome simplifier warning dependent on trace_simp.

Modified and shortened adm_disj lemmas.

Deleted a useless definition

Added optimization: do nothing for empty list

A bit more pattern-matching in eta_contract

Tidying and a corrected comment

Added a new challenge problem

Updated documentation of IFOL_ss

Documented thin_tac

Strengthened warnings concerning topthm(), etc.

Updated a reference

New class "order" and accompanying changes.

New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.

TFL: missing -q option!

tuned names: partial order, linear order;

tuned startup; semi fix of piping-quit peoblem (should work on systems with *real& sh);

fixed comment;

Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int

Renamed structure Int (intuitionistic prover) to IntPr

Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int

removed ISABELLE_INTERFACE_OPTIONS;

tuned; removed ISABELLE_INTERFACE_OPTIONS;

tuned; removed ISABELLE_SYMBOLS;

Modified proofs due to added triv_forall_equality.

Modified proofs because of added "triv_forall_equality".

Added "triv_forall_equality" to HOL_ss.

functionality added to getsettings;

removed getplatform, ISABELLE_OUTPUT_DIR;

removed getplatform, ISABELLE_OUTPUT_DIR;

removed getplatform;

integrated getplatform stuff; added ISABELLE_OUTPUT_DIR;

now falls back on ucat instead of cat;

improved usage msg;

added eq_sort (will move to sorts.ML eventually); added get_sort (handles constraints / defaults); attach_types: adapted to new get_sort;

adapted to new Syntax.read_typ;

adapted read_typ, simple_read_typ;

improved comments; raw_term_sorts: improved handling of sort constraints (consistency); added term_of_sort; renamed "_emptysort" to "_topsort"; preparations for marking of class idts;

added string_of_vname' (treats neg. index as free);