isabelle: Graph

fixed field_injects;
1998-10-21, by wenzelm
tuned;
1998-10-21, by wenzelm
no open;
1998-10-21, by wenzelm
tuned;
1998-10-21, by wenzelm
Tutorial
1998-10-21, by nipkow
dropped support for SML/NJ 109.x;
1998-10-21, by wenzelm
field_injects [iffs];
1998-10-21, by wenzelm
record_split_name;
1998-10-21, by wenzelm
tuned (all proofs are INSTABLE by David's definition of instability);
1998-10-21, by wenzelm
improved var names;
1998-10-21, by wenzelm
tuned stack_overflow_handler;
1998-10-20, by wenzelm
made SML/NJ happy;
1998-10-20, by wenzelm
delSWrapper "record_split_tac";
1998-10-20, by wenzelm
fixed Syntax module;
1998-10-20, by wenzelm
split_paired_all.ML;
1998-10-20, by wenzelm
field types: datatype;
1998-10-20, by wenzelm
quiet_mode, message;
1998-10-20, by wenzelm
quiet proofs;
1998-10-20, by wenzelm
fixed Syntax module;
1998-10-20, by wenzelm
Datatype instead of Prod;
1998-10-20, by wenzelm
QUIET_BREADTH_FIRST;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
no open;
1998-10-20, by wenzelm
simple Env replaced by Symtab;
1998-10-20, by wenzelm
added unvarify(T);
1998-10-20, by wenzelm
Syntax.max_pri;
1998-10-20, by wenzelm
Symtab.foldl;
1998-10-20, by wenzelm
quiet_mode, message;
1998-10-20, by wenzelm
structure Hidden = struct end;
1998-10-20, by wenzelm
hiding private stuff;
1998-10-20, by wenzelm
Symtab.foldl;
1998-10-20, by wenzelm
added foldl, keys;
1998-10-20, by wenzelm
split_paired_all.ML: turn surjective pairing into split rule;
1998-10-20, by wenzelm
updated
1998-10-20, by paulson
updated the MLWorks description
1998-10-20, by paulson
another little bug ;-) and minor changes in TLS.*;
1998-10-19, by mueller
little bug ;-)
1998-10-19, by mueller
added keyword 'and'
1998-10-19, by oheimb
corrected Header
1998-10-19, by oheimb
Addsimps [max_le_iff_conj];
1998-10-19, by nipkow
changed Super_L and Hyper_R to left and right Meta
1998-10-19, by oheimb
layout
1998-10-19, by oheimb
solved conflict by taking newest version;
1998-10-19, by mueller
added Clarify_tac to speed up proofs
1998-10-19, by paulson
moved a theorem
1998-10-19, by paulson
fixed comment
1998-10-19, by paulson
fixed some indenting; changed a VERY slow blast_tac to fast_tac
1998-10-19, by paulson
updated, tuned;
1998-10-18, by wenzelm
added Minho (Portugal);
1998-10-18, by wenzelm
Fixed bug (improper handling of flag flat_names).
1998-10-16, by berghofe
Added quiet_mode flag.
1998-10-16, by berghofe
- Changed structure of name spaces
1998-10-16, by berghofe
tuned MLWorks options;
1998-10-16, by wenzelm
MLWorks 2.0;
1998-10-16, by wenzelm
Changed structure of name spaces for datatypes.
1998-10-16, by berghofe
2. The simplifier now knows a little bit about nat-arithmetic.
1998-10-16, by nipkow
Mods because trans_tac is now part of thge simplifier.
1998-10-16, by nipkow
Mods because of: Installed trans_tac in solver of simpset().
1998-10-16, by nipkow
Installed trans_tac in solver of simpset().
1998-10-16, by nipkow
changed tags from 0, 1 to None, Some() to avoid special treatment of 0
1998-10-16, by paulson
parent is Main
1998-10-16, by paulson
*** empty log message ***
1998-10-16, by nipkow
integer simprocs
1998-10-15, by paulson
Uses overload_1st_set to specify overloading
1998-10-15, by paulson
specifications as sets of programs
1998-10-15, by paulson
Description of new version.
1998-10-14, by nipkow
New many-sorted version.
1998-10-14, by nipkow
See (* FIXME zero_neq_conv *)
1998-10-14, by nipkow
Nat: added zero_neq_conv
1998-10-14, by nipkow
added Int.int;
1998-10-13, by wenzelm
PRIVATE sig parts;
1998-10-13, by wenzelm
length_Suc_conv is no longer given to AddIffs
1998-10-13, by paulson
new theorems
1998-10-13, by paulson
tidied
1998-10-13, by paulson
Addition of HOL/UNITY/Client
1998-10-13, by paulson
new rule
1998-10-13, by paulson
Addition of HOL/UNITY/Client
1998-10-13, by paulson
Unified treatment of type error msgs.
1998-10-09, by nipkow
More pretty breaks in error msgs.
1998-10-09, by nipkow
Added a few breaks in error text.
1998-10-09, by nipkow
new theorem
1998-10-09, by paulson
new theorems
1998-10-09, by paulson
new guarantees laws
1998-10-09, by paulson
renamed Suc_card_Diff or something
1998-10-09, by nipkow
Multisets at last!
1998-10-09, by nipkow
added Induct/Multiset*
1998-10-09, by nipkow
New inductive definition of `card'
1998-10-09, by nipkow
polymorphic versions of nat_neq_iff and nat_neqE
1998-10-09, by paulson
Further improvement of the simplifier.
1998-10-08, by nipkow
Tuned simplifier not to re-normalized already normalized terms.
1998-10-07, by nipkow
tuned rm CVS;
1998-10-07, by wenzelm
runs test
1998-10-07, by nipkow
tidying and renaming
1998-10-07, by paulson
new theorems
1998-10-07, by paulson
tidied
1998-10-07, by paulson
new files UNITY/Comp.{thy,ML}
1998-10-07, by paulson
Merges FoldSet into Finite
1998-10-06, by nipkow
deleted incorrect code that set Goals.proof_timing:=false
1998-10-05, by paulson
Now prove_goalw_cterm never prints timing statistics
1998-10-05, by paulson
MLWorks demands the "op" before $
1998-10-05, by paulson
Finished proofs to end of section 5.1 of Chandy and Sanders
1998-10-05, by paulson
Join now an infix operator
1998-10-05, by paulson
simpler interface for Abel_Cancel
1998-10-05, by paulson
tidied
1998-10-05, by paulson
id <-> Id
1998-10-02, by nipkow
added Real to BasisLibrary
1998-10-02, by paulson
new file Provers/Arith/abel_cancel.ML
1998-10-02, by paulson
new files Provers/Arith/abel_cancel.ML and Real/simproc.ML
1998-10-02, by paulson
tidying
1998-10-02, by paulson
white border -- disabled;
1998-10-01, by wenzelm
Improved definition of foldSet.
1998-10-01, by nipkow
revised for new treatment of integers
1998-10-01, by paulson
new singleton_conv2
1998-10-01, by nipkow
tidied
1998-10-01, by paulson
a few new lemmas.
1998-10-01, by nipkow
composition theory
1998-10-01, by paulson
abstype of programs
1998-10-01, by paulson
now invokes functor
1998-10-01, by paulson
much tidying
1998-10-01, by paulson
new lemmas
1998-10-01, by paulson
better handling of literals
1998-10-01, by paulson
tidied
1998-10-01, by paulson
white space
1998-10-01, by paulson
new simproc functor
1998-10-01, by paulson
Revised version with Abelian group simprocs
1998-10-01, by paulson
handle empty name;
1998-09-29, by wenzelm
auto update
1998-09-29, by paulson
new function inter_term
1998-09-29, by paulson
Now id:(Acts prg) is implicit
1998-09-29, by paulson
modified proof for new simproc
1998-09-29, by paulson
many renamings and changes. Simproc for cancelling common terms in relations
1998-09-29, by paulson
New keywords
1998-09-29, by nipkow
Revised wf_acc_iff and Co.
1998-09-29, by nipkow
new: wfUNIVI
1998-09-29, by nipkow
Package now chooses type variable names more carefully to
1998-09-26, by berghofe
minor corrections
1998-09-25, by oheimb
exchanged automatic-tactics and semi-automatic-tactics
1998-09-25, by oheimb
improved indentation
1998-09-25, by oheimb
rearranged SIMPSET(');
1998-09-25, by wenzelm
*** empty log message ***
1998-09-25, by wenzelm
isatool logo;
1998-09-25, by wenzelm
added isatool logo;
1998-09-25, by wenzelm
improved;
1998-09-25, by wenzelm
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
added Int to BasisLibrary
1998-09-25, by paulson
deleted illegal "op"
1998-09-25, by paulson
uses BasisLibrary for Int.min
1998-09-25, by paulson
patched obsolete code
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*
1998-09-25, by paulson
Now uses integers instead of naturals
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
1998-09-25, by paulson
tuned;
1998-09-25, by wenzelm
tuned pretty_tag;
1998-09-25, by wenzelm
added REPEAT1;
1998-09-25, by wenzelm
create an instance of the Isabelle logo;
1998-09-24, by wenzelm
generic eps version;
1998-09-24, by wenzelm
simplified CLASIMP_DATA
1998-09-24, by oheimb
removed addcongs2 and delcongs2
1998-09-24, by oheimb
renamed mk_meta_eq to mk_eq
1998-09-24, by oheimb
simplified CLASIMP_DATA
1998-09-24, by oheimb
renamed some axioms; some new theorems
1998-09-24, by paulson
introduced addSE2, addSD2, addE2, and addD2
1998-09-24, by oheimb
improved description of looper and splitter
1998-09-24, by oheimb
workaround for litte bug in our ln command
1998-09-24, by oheimb
Function nat_of now maps negative integers to zero, not their absolute value
1998-09-24, by paulson
renamed some axioms
1998-09-24, by paulson
added correctness proofs for arithmetic
1998-09-24, by paulson
new induction rule for integers
1998-09-24, by paulson
fixed calls of ln, rm
1998-09-24, by oheimb
changed xnum token syntax;
1998-09-23, by wenzelm
unary minus
1998-09-23, by paulson
much renaming and reorganization
1998-09-23, by paulson
New directory Integ for the integers
1998-09-23, by paulson
a few new theorems
1998-09-23, by paulson
deleted needless parentheses
1998-09-23, by paulson
tidying and deleting needless parentheses
1998-09-23, by paulson
deleted needless parentheses
1998-09-23, by paulson
tuned Isamode;
1998-09-22, by wenzelm
re-organized for the new directory Integ
1998-09-22, by paulson
new directory for Integers
1998-09-22, by paulson
deleted erroneous semicolon
1998-09-22, by paulson
tidying
1998-09-22, by paulson
tidying
1998-09-22, by paulson
new directory for Integers
1998-09-22, by paulson
big tidying of simpsets, etc
1998-09-22, by paulson
*** empty log message ***
1998-09-21, by oheimb
improved addbefore and addSbefore
1998-09-21, by oheimb
*** empty log message ***
1998-09-21, by oheimb
added addD2, addE2, addSD2, and addSE2
1998-09-21, by oheimb
improved indentation
1998-09-21, by oheimb
added wrapper for bspec
1998-09-21, by oheimb
added addD2, addE2, addSD2, and addSE2
1998-09-21, by oheimb
re-added mem and list_all
1998-09-21, by oheimb
re-added mem and list_all
1998-09-21, by oheimb
added dependance on HOL
1998-09-21, by oheimb
added indentation
1998-09-21, by oheimb
simplified proof
1998-09-21, by oheimb
inserted space in #-1 to prevent confusion with an integer constant
1998-09-21, by paulson
Unary minus is now #- and not #~
1998-09-21, by paulson
much renaming and tidying
1998-09-21, by paulson
leaves subgoal package empty
1998-09-18, by paulson
improved (but still flawed) treatment of binary arithmetic
1998-09-18, by paulson
Now defines "int" as a linear order; basic derivations moved to IntDef
1998-09-18, by paulson
new files in Integ
1998-09-18, by paulson
simpler definition of zmagnitude, and new thms for it
1998-09-18, by paulson
stronger version of theI2
1998-09-18, by paulson
tidied
1998-09-18, by paulson
new theorem less_imp_Suc_add
1998-09-18, by paulson
new files in Integ
1998-09-18, by paulson
new theorem less_Suc_eq_le
1998-09-18, by paulson
new files in Integ
1998-09-18, by paulson
new theorem less_Suc_eq_le and le_simps
1998-09-18, by paulson
updated comments
1998-09-18, by paulson
tidying
1998-09-18, by paulson
theorem le_diff_conv2; tidying and expandshort
1998-09-18, by paulson
Pruning of parameters and True assumptions
1998-09-18, by paulson
Suppress timing messages for theorems proved in theory sections
1998-09-18, by paulson
improved error messages
1998-09-18, by paulson
deleted redundant quantifiers
1998-09-16, by paulson
From Compl(A) to -A
1998-09-15, by paulson
revised treatment of integers
1998-09-15, by paulson
From Compl(A) to -A
1998-09-15, by paulson
Function 'step' is already defined in NA.thy.
1998-09-15, by nipkow
tidied
1998-09-15, by paulson
commented out duplicate proof
1998-09-14, by paulson
simpler proof
1998-09-14, by paulson
new theorem le_diff_conv
1998-09-14, by paulson
Extra steps at end to make it run faster
1998-09-11, by paulson
added clarsimp_tac and Clarsimp_tac
1998-09-11, by oheimb
tidied using locales
1998-09-11, by paulson
Less deterministic reconstruction: now more robust but perhaps slower
1998-09-11, by paulson
tidied
1998-09-11, by paulson
fixed PROOF FAILED
1998-09-11, by paulson
fixed comment
1998-09-11, by paulson
stabilized proof of card_mono
1998-09-11, by oheimb
corrected indentation
1998-09-11, by oheimb
equals0D
1998-09-10, by paulson
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
1998-09-10, by paulson