merged Code_Generator.thy into HOL.thy

added a function partition and a few lemmas

added a few theorems about foldl and set

added lcm, ilcm (lcm for integers) and some lemmas about them;

included Class.thy in the compiling process for Nominal/Examples

remove simp attribute from lemma_STAR theorems

add lemma exp_of_real

tuned list comprehension

tuned;

added is_atomic; removed unused is_all;

added assume_rule_tac;

reverted appnd to append

authentic syntax for List.append

tuned comments

added a few comments to the proofs

removed fixmes

opaque-constraint removed

tuned;

monomorphic equality: let ML work out the details;

added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);

tuned Tactic signature;

removed obsolete Library.seq;

moved flip to library.ML; removed unused dest/unfold/unfold_rev; simplified fold/fold_rev/fold_map;

added CSUBGOAL;

cleaned up signature;

added downto0 (from library.ML);

merge_ss: plain merge of prems;

added flip (from General/basics.ML); renamed gen_submultiset to submultiset; moved downto0 to pattern.ML; moved legacy gen_merge_lists/merge_lists/merge_alists to Isar/locale.ML; moved plural to HOL/Tools/fundef_lib.ML; removed obsolete seq; simplified chop, fold2;

tuned document;

use antiquotations instead of raw TeX code; tuned document;

name_of_fqgar: precise type;

added plural (from Pure/library.ML); removed unused eq_str;

local open FundefLib;

renamed gen_submultiset to submultiset;

HOL-ex: tuned deps;

tuned list comprehension, added lemma

fixed tex error

*** empty log message ***

*** empty log message ***

extended

cosmetic

made SML/NJ happy;

added target/local_abbrev (from proof_context.ML); target_abbrev: demand equal head const (tool compliance);

moved specific target/local_abbrev to theory_target.ML;

"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases. more cleanup.

added "plural : 'a -> 'a -> 'b list -> 'a" for convenient error msg construction

proper handling of Tools;

cosmetic

refute_tac made more deterministic

extended

cosmetic

tracing disabled

additional tracing information

tuned

some tests for arith added

Moved list comprehension into List

MiniSAT mentioned in comment

fixed handling of meta-logic propositions

simplified interfaces, some restructuring

updated

added some bibtex entries

Added "merge-lemma" about wellfoundedness of unions (useful for some termination proofs)

Added simp-rules: "R O {} = {}" and "{} O R = {}"

rudimenary

tuned

dropped superfluous name bindings

localized

fixed typo

insert: canonical argument order;

simplified/unified list fold;

replace (- 1) with -1

simplify some proofs

tuned headers -- adapted to usual conventions;

moved Compute_Oracle from Pure/Tools to Tools;

proper theory setup for compute oracle (based on CPure); simplified oracle setup;

moved IsaPlanner from Provers to Tools; moved Compute_Oracle from Pure/Tools to Tools;

moved IsaPlanner from Provers to Tools;

made aconvc pervasive;

moved aconvc to more_thm.ML;

tuned ML setup;

decode_term: force qualified name into Const;

proper loading of ML files (in HOL.thy); moved Integ files to canonical place; misc cleanup;

HOL_proofs;

moved Integ files to canonical place;

proper loading of ML files;

removed dead code;

tuned header;

doc: exclude isabelle_isar.pdf;

tuned the proof

introduced symmetric variants of the lemmas for alpha-equivalence

proper loading of ML files; removed obsolete IFOL.thy/FOL.thy values;

removed obsolete IFOL.thy/FOL.thy values;

proper loading of ML files;

tuned header;

tuned oracle setup;

moved HOLCF tools to canonical place;

moved TFL files to canonical place;

moved TFL files to canonical place;

added src/Tools; moved TFL files to canonical place;

fixed title;

Tools: generic tools outside of Pure.

moved Integ files to canonical place;

fixed use_thy "LocalWeakening";

included new example in the compiling process

a theory using locally nameless terms and strong induction principles

tuned the proof

emulate later version of TextIO.inputLine;

reversed SML B library patches;

TextIO.inputLine: use present SML B library version;

tuned USEDIR_OPTIONS; PDF_VIEWER: try to be smart for MacOS (Darwin);

removed HOL4 image, which seldom works;

simplified data setup

instance: always print sorts on failure

more example

fixed typo

updated

generalized lemmas

eliminated strings

tuned

clarified error message