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);

cd made readably again;

tuned;