*** empty log message ***

*** empty log message ***

inputs Even.tex

minor tinkering

Even numbers section of Inductive chapter

tuned msg;

antiquotation "goals": error message;

* support sub/super scripts (for single symbols only), input syntax is like this: "A\<^sup>*" or "A\<^sup>\<star>"; * antiquotation @{goals} for output of *dynamic* goals state; Note that presentation of goal states does not conform to actual human-readable proof documents. Please do not include goal states into document output unless you really know what you are doing!

let commands access Toplevel.state; added command "goals" and option "goals_limit";

added pretty_goals;

added antiquotation "goals" and option "goals_limit"; tuned;

tuned;

added clasimpset: unit -> clasimpset;

tuned;

Acc example

even numbers example

intro_classes by default; tuned;

declare trancl rules;

tuned;

updated;

intro_classes by default;

make sure default document works;

comment out Pure-copied target;

* HOL: default proof step now includes 'intro_classes';

*** empty log message ***

part of set-up

sets chapter

fixed crossref

tidied

X-symbol

auto gen

addition of Rules, Sets and some macros of lcp

goodbye to this dummy file

now includes Rules, Sets (?)

the Rules chapter and theories

the Sets chapter and theories

quantifiers now allowed in inductive defs

tidied

isatool unsymbolize;

added type_definitionI;

tuned deps;

contrapos

two spelling fixes

tuned;

simplified quotients (only plain total equivs);

tuned;

*** empty log message ***

tuned;

*** empty log message ***

provide more theorems (see subset.thy); tuned;

InductAttrib;

improved typedef; tuned proofs;

improved typedef; tuned;

added theory for HOL type definitions;

tuned;

added Tools/induct_attrib.ML;

declare sym [elim?] in HOL.ML instead of Calculation.thy;

tuned \isasymuniqex;

split over two files: induct_attrib.ML, induct_method.ML;

tuned;

use RecdefPackage.tcs_of;

added tcs_of;

updated;

removed Library/Accessible_Part.ML;

use Multiset from HOL/Library;

use Accessible_Part from HOL/Library;

path_add "~~/src/HOL/Library";

tuned;

tuned declarations;

avoid "_" and "^" (more robust);

removed Acc and Multiset (see HOL/Library);

moved to HOL/Library;

MultisetOrder mmoved to HOL/Library;

moved to HOL/LIbrary;

added HOL/Library, rearranged several files;

moved to HOL/Library;

"The Supplemental Isabelle/HOL Library";

added path_add;

A general ``while'' combinator (from main HOL);

Quotient types;

Multisets (from HOL/Induct/Multiset and friends);

The accessible part of a relation (from HOL/Induct/Acc);

\isabellecontext: output_syms;

restart: do not reset theory loader path;

* HOL/Library: a collection of generic theories to be used together with main HOL; the theory loader path already includes this directory by default; the following existing theories have been moved here: HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While (as While_Combinator);

*** empty log message ***

*** empty log message ***

*** empty log message ***

wellfounded -> well-founded

tuned;

"Deriving rules";

improved;

*** empty log message ***

*** empty log message ***

renaming of contrapos rules

tidied some awkward proofs

tidying; removed unused rev_contra_subsetD

restoration of "equalityI"; renaming of contrapos rules

renaming of contrapos rules

tidying and renaming of contrapos rules

cosmetics

added intermediate value thms

<= -> \<le>

updated;

*** empty log message ***

*** empty log message ***

tuned;

fixed \isasyminv;

more elements;

proper symbol markup with \isamath, \isatext; support sub/super scripts:

*** empty log message ***

*** empty log message ***

*** empty log message ***

renamed fp_Tarski to fp_unfold

*** empty log message ***

*** empty log message ***

*** empty log message ***

*** empty log message ***

updated;

induct -> lfp_induct;