isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
1997-05-30, by paulson
Overloading of "^" requires a type constraint
1997-05-30, by paulson
Overloading of "^" requires new type class "power", with types "nat" and
1997-05-30, by paulson
New theory Divides
1997-05-30, by paulson
Many new theorems about cardinality
1997-05-30, by paulson
Now Divides must be the parent
1997-05-30, by paulson
Moving div and mod from Arith to Divides
1997-05-30, by paulson
flushOut ensures that no recent error message are lost (not certain this is
1997-05-30, by paulson
polyml-3.1 default again (for local work);
1997-05-27, by wenzelm
fixed -P (checkout only);
1997-05-27, by wenzelm
NJ 1.09.2x as factory default! Isabelle94-8
1997-05-27, by wenzelm
Last changes for new release 94-8
1997-05-27, by mueller
added 1.09.28 note;
1997-05-27, by wenzelm
New theorems suggested by Florian Kammueller
1997-05-27, by paulson
Restoration of the two "bypassed" theorems Union_quotient and quotient_disj
1997-05-27, by paulson
Removal of card_insert_disjoint, which is now a default rewrite rule
1997-05-27, by paulson
New theorem disjoint_eq_subset_Compl
1997-05-27, by paulson
New theorem le_Suc_eq
1997-05-27, by paulson
Removal of mask.sig and mask.sml
1997-05-27, by paulson
Removal of module Mask and datatype binding with its constructor |->
1997-05-27, by paulson
New theorems suggested by Florian Kammueller
1997-05-27, by paulson
remoded ccc1
1997-05-26, by slotosch
removed ccc1
1997-05-26, by slotosch
tuned comment;
1997-05-26, by wenzelm
Two useful facts about Powersets suggested by Florian Kammueller
1997-05-26, by paulson
Added a missing "result();" after problem 43.
1997-05-26, by paulson
Tidying using the new exhaust_tac
1997-05-26, by paulson
Now recdef checks the name of the function being defined.
1997-05-26, by paulson
Deleted option_case_tac because exhaust_tac performs a similar function.
1997-05-26, by paulson
Renamed lessD to Suc_leI
1997-05-26, by paulson
New operator "lists" for formalizing sets of lists
1997-05-26, by paulson
New theorem subset_inj_onto
1997-05-26, by paulson
Two results suggested by Florian Kammueller
1997-05-26, by paulson
Tidying and a couple of useful lemmas
1997-05-26, by paulson
Added recdef
1997-05-26, by paulson
Primrec: New example ported from ZF
1997-05-26, by paulson
Renamed lessD to Suc_leI
1997-05-26, by paulson
New example ported from ZF
1997-05-26, by paulson
Simplified proofs using expand_option_case
1997-05-26, by paulson
Now checks the name of the function being defined;
1997-05-26, by paulson
More de-HOL-ification
1997-05-26, by paulson
Now checks the name of the function being defined
1997-05-26, by paulson
Deleted unused functions
1997-05-26, by paulson
Now a Perl script. No longer requires commands to be at the beginnings of
1997-05-26, by paulson
Slight simplifications
1997-05-26, by paulson
Eliminated ccc1. Moved ID,oo into Cfun.
1997-05-25, by slotosch
Moved the classes flat chfin from Fix to Pcpo.
1997-05-25, by slotosch
*** empty log message ***
1997-05-25, by slotosch
Eliminated the prediates flat,chfin
1997-05-25, by slotosch
eliminated the constant less by the introduction of the axclass sq_ord
1997-05-25, by slotosch
tuned;
1997-05-23, by wenzelm
arbitrary
1997-05-23, by nipkow
Added `arbitrary'
1997-05-23, by nipkow
fixed;
1997-05-23, by wenzelm
new syntactic priority of lambda abstraction
1997-05-23, by oheimb
adapted entry for addss, addSss
1997-05-23, by oheimb
news.
1997-05-23, by nipkow
Documented `size' function for datatypes.
1997-05-23, by nipkow
fixed a bug
1997-05-23, by mueller
removed TFL from test;
1997-05-23, by wenzelm
remove cl.cam font server;
1997-05-23, by wenzelm
exec the emacs;
1997-05-23, by wenzelm
Base theory is now Arith, not Nat. (because all datatypes now require Arith).
1997-05-23, by nipkow
All datatypes now require Arith.
1997-05-23, by nipkow
Added overloaded function `size' for all datatypes.
1997-05-23, by nipkow
exhaust_tac can now deal with whole terms rather than just variables.
1997-05-22, by nipkow
added href to Isamode;
1997-05-22, by wenzelm
fixed doc;
1997-05-22, by wenzelm
adapted to Isamode 2.6;
1997-05-22, by wenzelm
tuned Isamode stuff;
1997-05-22, by wenzelm
New headers and other minor changes
1997-05-22, by paulson
Now the recdef induction rule variables are named u, v, ...
1997-05-22, by paulson
New example of recdef and permutative rewriting
1997-05-22, by paulson
Now uses type option instead of Fail/Subst
1997-05-22, by paulson
Now uses type option instead of Fail/Subst
1997-05-22, by paulson
Uses option_case_tac
1997-05-22, by paulson
Deleted rprod: lex_prod is (usually?) enough
1997-05-22, by paulson
Deleted obsolete proofs. But option_case_tac will be obsolete too
1997-05-22, by paulson
New example: ex/Fib
1997-05-22, by paulson
New lemmas used for ex/Fib
1997-05-22, by paulson
Added rotation to exhaust_tac.
1997-05-22, by nipkow
tuned;
1997-05-22, by wenzelm
added;
1997-05-22, by wenzelm
tuned;
1997-05-22, by wenzelm
SYNC;
1997-05-22, by wenzelm
Documented exhaust_tac.
1997-05-22, by nipkow
fixed packages;
1997-05-22, by wenzelm
fixed packages;
1997-05-22, by wenzelm
tuned comments;
1997-05-22, by wenzelm
Replaced res_inst-list_cases by generic exhaust_tac.
1997-05-22, by nipkow
Added exhaustion thm and exhaust_tac for each datatype.
1997-05-22, by nipkow
fixed find cmd;
1997-05-21, by wenzelm
set version;
1997-05-21, by wenzelm
tuned all READMEs;
1997-05-21, by wenzelm
release version (sort of);
1997-05-21, by wenzelm
SYNC;
1997-05-21, by wenzelm
fixed spelling;
1997-05-21, by wenzelm
changes for release 94-8
1997-05-21, by mueller
tuned;
1997-05-21, by wenzelm
Code tidying: removal of C combinator
1997-05-21, by paulson
Basis library input/output primitives; \!simpset instead of HOL_ss
1997-05-21, by paulson
Basis library input/output primitives; currying the induction rule;
1997-05-21, by paulson
TFL induction rule is now curried
1997-05-21, by paulson
Function "sum" now defined using primrec
1997-05-21, by paulson
Mostly cosmetic changes: updated headers, ID lines, etc.
1997-05-21, by paulson
Removed rprod from the WF relation
1997-05-21, by paulson
Removed rprod from the WF relation; simplified proofs;
1997-05-21, by paulson
Replaced Konrad's own add_term_names by the predefined one.
1997-05-21, by nipkow
tuned command line;
1997-05-20, by wenzelm
tuned;
1997-05-20, by wenzelm
under construction;
1997-05-20, by wenzelm
SYNC;
1997-05-20, by wenzelm
fix spelling;
1997-05-20, by wenzelm
the new README;
1997-05-20, by wenzelm
now generated automatically from README.html;
1997-05-20, by wenzelm
README generation;
1997-05-20, by wenzelm
removed Cambridge font server;
1997-05-20, by wenzelm
fixed bash path;
1997-05-20, by wenzelm
reset make_html afterwards;
1997-05-20, by wenzelm
fixed spelling;
1997-05-20, by wenzelm