2008-11-16 wenzelm 2008-11-16 put_name/thm_proof: promises are filled with fulfilled proofs; tuned;
2008-11-16 wenzelm 2008-11-16 proof_body/pthm: removed redundant types field; fold_proof_atoms: unified recursive case with fold_body_thms; tuned signature;
2008-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-16 berghofe 2008-11-16 - Corrected order of quantification over Frees. - Fixed bug in handling of TFrees that caused variable order to get mixed up.
2008-11-16 berghofe 2008-11-16 Frees in PThms are now quantified in the order of their appearance in the proposition as well, to make it compatible (again) with variable order used by forall_intr_frees.
2008-11-15 wenzelm 2008-11-15 adapted PThm and MinProof;
2008-11-15 wenzelm 2008-11-15 retrieve thm deps from proof_body; removed obsolete enable/disable operation;
2008-11-15 wenzelm 2008-11-15 retrieve thm deps from proof_body;
2008-11-15 wenzelm 2008-11-15 adapted PThm;
2008-11-15 wenzelm 2008-11-15 proof_of_term: removed obsolete disambiguisation table; adapted PThm; Thm.proof_of returns proof_body;
2008-11-15 wenzelm 2008-11-15 rewrite_proof: simplified simprocs (no name required); adapted PThm; fold_proof_atoms;
2008-11-15 wenzelm 2008-11-15 Thm.proof_of returns proof_body; adapted PThm;
2008-11-15 wenzelm 2008-11-15 refined notion of derivation, consiting of promises and proof_body; removed oracle_of (would require detailed check wrt. promises); proof_of returns proof_body;
2008-11-15 wenzelm 2008-11-15 reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial); added type proof_body, which covers oracles and thms of local proof; added general fold_body_thms, fold_proof_atoms; removed thms_of_proof, thms_of_proof', axms_of_proof; slightly more abstract handling of body content (oracles, thms); rewrite_proof: simplified simprocs (no name required); thm_proof: lazy fulfillment of promises;
2008-11-15 wenzelm 2008-11-15 pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
2008-11-15 wenzelm 2008-11-15 ProofSyntax.proof_of_term: removed obsolete disambiguisation table; adapted PThm;
2008-11-15 wenzelm 2008-11-15 name_of_thm: Proofterm.fold_proof_atoms; Thm.proof_of returns proof_body;
2008-11-15 wenzelm 2008-11-15 Thm.proof_of returns proof_body;
2008-11-15 wenzelm 2008-11-15 clean: added HOL-Main;
2008-11-15 wenzelm 2008-11-15 rewrite_proof: simplified simprocs (no name required);
2008-11-15 wenzelm 2008-11-15 multithreading support for polyml-5.2 actually disabled -- as advertized;
2008-11-14 ballarin 2008-11-14 Initial part of locale reimplementation.
2008-11-14 ballarin 2008-11-14 Made local_note_prefix public.
2008-11-14 haftmann 2008-11-14 re-educated guess
2008-11-14 haftmann 2008-11-14 namify and name_decl combinators
2008-11-14 haftmann 2008-11-14 Name.is_nothing
2008-11-14 haftmann 2008-11-14 lemmas about dom and minus / insert
2008-11-14 haftmann 2008-11-14 added length_unique operation for code generation
2008-11-13 wenzelm 2008-11-13 updated generated files;
2008-11-13 wenzelm 2008-11-13 removed "includes" element (lost update?);
2008-11-13 wenzelm 2008-11-13 updated generated files;
2008-11-13 wenzelm 2008-11-13 added section "Explicit instantiation within a subgoal context";
2008-11-13 wenzelm 2008-11-13 renamed "Rules" to "Object-level rules";
2008-11-13 wenzelm 2008-11-13 more on basic tactics;
2008-11-13 wenzelm 2008-11-13 basic ML reference for tactics;
2008-11-13 wenzelm 2008-11-13 added section "Tactics";
2008-11-13 wenzelm 2008-11-13 more contributors;
2008-11-13 wenzelm 2008-11-13 separate section "Inspecting the syntax" for print_syntax;
2008-11-13 wenzelm 2008-11-13 misc tuning of inner syntax;
2008-11-13 wenzelm 2008-11-13 added inner lexical syntax, reusing outer one;
2008-11-13 wenzelm 2008-11-13 misc tuning;
2008-11-13 wenzelm 2008-11-13 tuned outer lexical syntax; fixed var/tvar: really need question marks here;
2008-11-13 wenzelm 2008-11-13 more tuning of Pure grammer;
2008-11-13 wenzelm 2008-11-13 updated and elaborated Pure grammer;
2008-11-13 wenzelm 2008-11-13 added Pure grammer (from old ref manual);
2008-11-13 wenzelm 2008-11-13 mixfix annotations: verbatim for special symbols;
2008-11-13 wenzelm 2008-11-13 added section "The Pure grammar" (incomplete version, based on old ref manual);
2008-11-13 wenzelm 2008-11-13 added section "Priority grammars" (variant from old ref manual);
2008-11-13 wenzelm 2008-11-13 added section "Co-regularity of type classes and arities" (variant from old ref manual); tuned arity spacing;
2008-11-13 wenzelm 2008-11-13 minor tuning (according to old ref manual);
2008-11-13 wenzelm 2008-11-13 misc tuning and rearrangement of section "Printing logical entities";
2008-11-13 wenzelm 2008-11-13 misc tuning and rearrangement of section "Printing logical entities";
2008-11-13 wenzelm 2008-11-13 fixed/tuned syntax for attribute "tagged";
2008-11-13 wenzelm 2008-11-13 added pretty printing options (from old ref manual);
2008-11-13 wenzelm 2008-11-13 separate chapter "Inner syntax --- the term language";
2008-11-13 wenzelm 2008-11-13 updated/refined types of Isar language elements, removed special LaTeX macros;
2008-11-13 wenzelm 2008-11-13 unified use of declaration environment with IsarImplementation; tuned ML decls;
2008-11-13 wenzelm 2008-11-13 ignore ThyOutput.source flag;
2008-11-13 wenzelm 2008-11-13 added bind_thm, bind_thms;
2008-11-13 wenzelm 2008-11-13 tuned section "Incorporating ML code"; moved method_setup to separate section "Defining proof methods";