instances for class discrete_cpo

new lemma cont_discrete_cpo

new discrete_cpo axclass

temporary adjustions

explicit del_funcs

proper term_of functions

avoiding dynamic simpset lookup

new lemma is_lub_Pair; cleaned up some proofs

commented stuff out

added multiset comprehension

idempotent semigroups

dual orders and dual lattices

Theorem Inductive.lfp_ordinal_induct generalized to complete lattices

new term-building combinators

cleaned up evaluation interfaces

tuned names

treating division by zero properly

eliminated escaped white space;

basic scanners: produce symbol list instead of imploded string; tuned signature;

* Outer syntax: string tokens no longer admit escaped white space;

location_of_position: Position.column_of (which counts Isabelle symbols, not characters);

added count/counted: improved position handling for token syntax; removed obsolete incr_line/keep_line/scan_blank; string tokens no longer admit escaped white space, which was an accidental (undocumented) feature;

added column field; replaced inc by general advance operation; str_of: no output for file without line information;

T.count/counted: improved position handling for token syntax;

added column property;

removed redundant repeatd scanner combinator;

added ::: / @@@ scanner combinators;

Tuned uniqueness proof for recursion combinator.

Cleaned up simproc code.

tuned the proof of the substitution lemma

rename_client_map_tac: avoid ill-defined thm reference;

use_thy: do not set implicit ML context anymore;

added ambiguity_limit (restricts parse trees / terms printed in messages); tuned;

renamed thms_containing_limit to FindTheorems.limit;

eliminated some legacy ML files;

added bind_thms;

tuned;

removed legacy ML file;

syntax error: unified output of priorities;

syntax error: reduced spam -- print expected nonterminals instead of terminals; tuned pretty_gram;

avoid redundant escaping of Isabelle symbols;

grouped versions of axioms/define/notes;

misc tuning and internal rearrangement; tuned attribute syntax -- no need for eta-expansion;

added theorem group property;

added theorem group operations; note_thmss: add kind to *all* intermediate thms; get_kind: default to empty name;

added surround;

tuned attribute syntax -- no need for eta-expansion;

added theorem group;

internal inductive: fresh theorem group;

modernized primrec;

Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections; more simultaneous use_thys;

modernized primrec;

tuned document; modernized primrec;

tuned document;

tuned;

* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;

tuned

print postprocessor equations

fixed and tuned

dropped superfluous code theorems

improved code theorem setup

consistent interacitve bootstrap of HOL-Main

distinguished examples for Efficient_Nat.thy

clarified setup of method "normalization"

moved definition of power on ints to theory Int

removed unused properties; replaced ContextPosition by Position.thread_data;

replaced ContextPosition by Position.thread_data;

statement: keep explicit position; replaced ContextPosition by Position.thread_data;

improved apply: handle thread position, apply to context here; replaced ContextPosition by Position.thread_position;

removed unused Toplevel.properties;

added combinator for wrapped lazy evaluation;

added setmp_thread_data_seq;

removed obsolete context_position.ML (superseded by Position.thread_data);

switched to polyml-cvs;

Reimplemented proof of strong induction theorem.

Added lemma at_fin_set_fresh.

reactivated mk of java/scala sources, with paranoia PATH setting for sunbroy;

exceptions: assign result = null properly;

tuned proofs;

recovered #der example without using val it;

yet another OCaml fix

tuned

added map_split

added class semiring_div

fixed OCaml

avoid 'it' in ML expressions

Removed Logic.auto_rename.

Efficient_Nat streamlined and improved

tuned proof

non-negative numerals

tuned

more lemmas

proper meaningful examples

explicit auxiliary function for code setup

streamlined and improved

adjusted to constant and theorem renames

avoiding direct references to numeral presentation

tuned code setup

add space to binder syntax

pcpodef generates strict_iff lemmas

change lemma admD to rule_format

improved implementation

convert lemma lub_mono to rule_format

rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less

change class axiom chfin to rule_format

change class axiom ax_flat to rule_format

joined theories IntDef, Numeral, IntArith to theory Int

tuned

further localization

explicit code lemma for implication

add instance for class bifinite

clean up some proofs; add lemmas spair_strict_iff, spair_less_iff, spair_eq_iff; add instance for class bifinite

declare cpair_strict [simp]

make at-sml-dev experimental

added bifinite class instance

add bifinite instances

add class bifinite_cpo for possibly-unpointed bifinite domains

cleaned up instance proofs

new-style instantiation proof for unit :: po

class bifinite supersedes class dcpo; remove unnecessary dcpo stuff