isabelle: Graph

Tidying of signature. More robust renaming in freeze_thaw.
1997-06-05, by paulson
Removal of freeze_vars and thaw_vars (quite unused...)
1997-06-05, by paulson
Removal of radixstring from string_of_int; addition of string_of_indexname
1997-06-05, by paulson
There was never need for another copy of radixstring...
1997-06-05, by paulson
Numerous simplifications and removal of HOL-isms
1997-06-05, by paulson
Now loads theory Recdef
1997-06-05, by paulson
A slight simplification of optstring
1997-06-05, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
1997-06-05, by paulson
Deleted the obsolete "pred_list" relation
1997-06-05, by paulson
Documented the new distinct_subgoals_tac
1997-06-05, by paulson
A slight simplification of optstring
1997-06-05, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
1997-06-05, by paulson
Made the pseudo-type of split_rule_var a separate argument
1997-06-05, by paulson
eliminated non-ASCII;
1997-06-04, by wenzelm
eliminated freeze_vars;
1997-06-04, by wenzelm
changed priority of -> from [6,5]5 to [1,0]0
1997-06-04, by mueller
is_blank: fixed space2;
1997-06-03, by wenzelm
No longer refers to internal TFL structures
1997-06-03, by paulson
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
1997-06-03, by paulson
New theory "Power" of exponentiation (and binomial coefficients)
1997-06-03, by paulson
New theorem about the cardinality of the powerset (uses exponentiation)
1997-06-03, by paulson
Type inference makes a Const here, perhaps elsewhere?thry.sml
1997-06-02, by paulson
poly_tvars allows recdefs to be made without type constraints
1997-06-02, by paulson
Corrected banner: it is W0, not MiniML
1997-06-02, by paulson
New statement and proof of free_tv_subst_var in order to cope with new
1997-06-02, by paulson
Now Un_insert_left, Un_insert_right are default rewrite rules
1997-06-02, by paulson
Corrected statement of filter_append; added filter_size
1997-06-02, by paulson
Simplified proof
1997-06-02, by paulson
New theorems le_add_diff_inverse, le_add_diff_inverse2
1997-06-02, by paulson
trivial changes to incorporate CTL.thy and Example.ML in html file;
1997-05-30, by mueller
Simplified the calling sequence of CONTEXT_REWRITE_RULE
1997-05-30, by paulson
Moved "less_eq" to NatDef from Arith
1997-05-30, by paulson
New results including the basis for unique factorization
1997-05-30, by paulson
Now "primes" is a set
1997-05-30, by paulson
Now Divides must be the parent
1997-05-30, by paulson
New proofs about cardinality. Suggested by Florian Kammueller
1997-05-30, by paulson
Addition of Finite as parent allows cardinality theorems
1997-05-30, by paulson
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
IMPORTANT NOTE: This is the old README.
1997-05-20, by wenzelm
X11 font server sample configuration;
1997-05-20, by wenzelm
deleted duplicate rewrite rules of lift.simps
1997-05-20, by mueller
minor changes
1997-05-20, by mueller
tuned;
1997-05-20, by wenzelm
added eindhoven http address
1997-05-20, by mueller
Declares Option_ as synonym for structure Option
1997-05-20, by paulson
Removal of redundant code (unused or already present in Isabelle.
1997-05-20, by paulson
Basis library version of type "option" now resides in its own structure Option
1997-05-20, by paulson
Removal of ex/LexProd
1997-05-20, by paulson
Renamed egcd and gcd; defined the gcd function using TFL
1997-05-20, by paulson
Removal of duplicate code from TFL
1997-05-20, by paulson
New arithmetic laws let us delete three lines of a proof
1997-05-20, by paulson
Added comment: it is SLOW
1997-05-20, by paulson
Some theorems moved to HOL/Arith.ML
1997-05-20, by paulson
Relation "less_than" internalizes "<" for easy use of TFL
1997-05-20, by paulson
New pattern-matching definition of pred_nat
1997-05-20, by paulson
The diff laws must be named: we do "Delsimps [diff_Suc];"
1997-05-20, by paulson
New theorems from Hoare/Arith2.ML
1997-05-20, by paulson
new treatment of Prover files
1997-05-20, by paulson
Removal of ex/LexProd; TFL files; new treatment of Prover files
1997-05-20, by paulson
Removal of ex/LexProd
1997-05-20, by paulson
improved output syntax of op =, op ~= (more parentheses);
1997-05-20, by wenzelm
SYNC;
1997-05-20, by wenzelm
index: model checkers;
1997-05-20, by wenzelm
*** empty log message ***
1997-05-20, by wenzelm
SYNC;
1997-05-20, by wenzelm
little changes
1997-05-20, by mueller
Documented auto_tac
1997-05-19, by paulson
Section numbers may now be nested three deep, as in 1.2.3
1997-05-19, by paulson
Distributed Psubset stuff to basic set theory files, incl Finite.
1997-05-16, by nipkow
renamed unsafe_addss to addss
1997-05-16, by oheimb
readme added
1997-05-16, by mueller
commented out qed (in case the MC is unavailable);
1997-05-16, by mueller
added Modelcheck example;
1997-05-16, by mueller
still under construction!
1997-05-16, by wenzelm
improved www4 ref;
1997-05-16, by wenzelm
fixed infix syntax;
1997-05-16, by wenzelm
fixed Modelchek reference;
1997-05-16, by wenzelm
SYNC;
1997-05-16, by wenzelm
hint at more sections;
1997-05-16, by wenzelm
added \settdx;
1997-05-16, by wenzelm
Invoking Model Checkers in Isabelle/HOL;
1997-05-16, by mueller
renamed unsafe_addss to addss
1997-05-16, by oheimb
Subst now moved to directory HOL
1997-05-16, by paulson
renamed unsafe_addss to addss
1997-05-15, by oheimb
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
1997-05-15, by oheimb
*** empty log message ***
1997-05-15, by wenzelm
corrected depth_tac: no call for safe_step_tac if subgoal not present
1997-05-15, by oheimb
fixed bash path!!!
1997-05-15, by wenzelm
SYNC;
1997-05-15, by wenzelm
removed garbage;
1997-05-15, by wenzelm
sysman refs;
1997-05-15, by wenzelm
remove FIXME;
1997-05-15, by wenzelm
New proofs for TFL
1997-05-15, by paulson
Improved error message in "require_thy"
1997-05-15, by paulson
Added pred_list for TFL
1997-05-15, by paulson
Preliminary TFL versions
1997-05-15, by paulson
TFL theory section
1997-05-15, by paulson
New theories used by TFL
1997-05-15, by paulson
New version, modified by Konrad Slind and LCP for TFL
1997-05-15, by paulson
TFL now integrated with HOL (more work needed)
1997-05-15, by paulson
remove Witness.thy;
1997-05-15, by wenzelm
SYNC;
1997-05-14, by wenzelm
preliminary!
1997-05-14, by wenzelm
added \tooldx;
1997-05-14, by wenzelm
tuned comment;
1997-05-14, by wenzelm