assumption / finish: handle non-atomic assumptions from context as well;

added atomic_judgment;

structure Obtain = Obtain;

new lemma card_Diff2_less for mulilated chess board

*** empty log message ***

*** empty log message ***

*** empty log message ***

the section command will belong to the new file

advanced induction examples

auto update?

replaced Acc.thy by Advanced.thy

no longer needed: too complicated an example

*** empty log message ***

auto generated

tuned goal output;

*** empty log message ***

*** empty log message ***

updated;

tuned goals output;

improved statement bindings for props; tuned;

converse: syntax \<inverse>;

tuned;

added ex/PER.thy;

improved doc of "subgoals" antiquotation;

replaced \isasymmacron by \isasyminverse;

tuned tex template;

Partial equivalence relations (leftover from HOL/Quot);

added antiq. subgoals

Added antiquotation "subgoals".

Mod because of additional parameters to pretty_goals.

back to 1.167, due to Emacs/CVS casualty!!;

added instantiate_tac

*** empty log message ***

removed isabelle resources: are available from main pages

cleanup, looks ok now with konqueror, too

*** empty log message ***

*** empty log message ***

added the $Id:$ line

*** empty log message ***

*** empty log message ***

use Library/List_Prefix;

added HOL/Library/List_Prefix;

improved antiquotations;

added \isarantiq;

add \<le> to list of "good" symbols;

tuned names;

added List_Prefix;

more "xsymbols" syntax;

"List prefixes" library theory (replaces old Lex/Prefix);

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