isabelle: Graph

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

updated to Isabelle98;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
added files containing temproal logic and abstraction;
1998-01-12, by mueller
Delsimprocs nat_cancel;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
Tidying, mostly to do with handling a more specific version of Fake_parts_insert
1998-01-12, by paulson
tuned;
1998-01-12, by wenzelm
tuned;
1998-01-12, by wenzelm
fixed author;
1998-01-12, by wenzelm
Simplified proofs by omitting PA = {|XA, ...|} from RA2
1998-01-10, by paulson
trivial tidy
1998-01-10, by paulson
tuned;
1998-01-09, by wenzelm
automatic index.html patch;
1998-01-09, by wenzelm
tuned;
1998-01-09, by wenzelm
tuned ISABELLE_TMP_PREFIX;
1998-01-09, by wenzelm
thm_ord;
1998-01-09, by wenzelm
eliminated make_ord;
1998-01-09, by wenzelm
ISABELLE_TMP_PREFIX: $LOGNAME
1998-01-09, by wenzelm
several minor updates;
1998-01-09, by wenzelm
tuned;
1998-01-08, by wenzelm
index.html for Isabelle Distribution Area;
1998-01-08, by wenzelm
updated to Isabelle98;
1998-01-08, by wenzelm
tuned;
1998-01-08, by wenzelm
fixed thm_less;
1998-01-08, by wenzelm
Expressed most Oops rules using Notes instead of Says, and other tidying
1998-01-08, by paulson
added split_paired_Ex to the implicit simpset
1998-01-08, by oheimb
added select_equality to the implicit claset
1998-01-08, by oheimb
added select_equality to the implicit claset
1998-01-08, by oheimb
added newline at end of file
1998-01-08, by oheimb
*** empty log message ***
1998-01-08, by oheimb
streamlined specification of included theories
1998-01-08, by oheimb
corrected Title
1998-01-08, by oheimb
removed obsolete comment
1998-01-08, by oheimb
added Univalent
1998-01-08, by oheimb
removed Eps_eq, ex1_Eps_eq, and some unnecessary parentheses
1998-01-08, by oheimb
added update_same, update_other, update_triv, and map_of_SomeD
1998-01-08, by oheimb
replaced fn _ => by K
1998-01-08, by oheimb
*** empty log message ***
1998-01-08, by wenzelm
New rule: image_subset
1998-01-08, by paulson
Restored the ciphertext in OR4 in order to make the spec closer to that in
1998-01-08, by paulson
Tidied by adding more default simprules
1998-01-08, by paulson
adapted to new split order;
1998-01-07, by wenzelm
adapted to new sort function;
1998-01-07, by wenzelm
improved targets;
1998-01-07, by wenzelm
tuned;
1998-01-06, by wenzelm
added -u option (again);
1998-01-05, by wenzelm
Now calls Blast_tac more often
1998-01-05, by paulson
obsolete;
1998-01-02, by wenzelm
feeder;
1998-01-02, by wenzelm
Changed required by new blast_tac (the one that squashes flex-flex pairs)
1998-01-02, by paulson
Blast_tac now squashes flex-flex pairs immediately
1998-01-02, by paulson
New theorem image_subsetI
1998-01-02, by paulson
Making proofs faster, especially using keysFor_parts_insert
1998-01-02, by paulson
do require perl;
1998-01-02, by wenzelm
Auto_tac now has type tactic, not unit->tactic
1998-01-02, by paulson
Declared startTiming and endTiming
1998-01-02, by paulson
use feeder to pipe into ML;
1997-12-31, by wenzelm
removed -i option;
1997-12-31, by wenzelm
nth -> !
1997-12-30, by nipkow
nth -> !
1997-12-30, by nipkow
feed isabelle session;
1997-12-29, by wenzelm
commented out symboloutput.pl;
1997-12-29, by wenzelm
added feeder.pl;
1997-12-29, by wenzelm
pretty_name_space;
1997-12-29, by wenzelm
removed declared;
1997-12-29, by wenzelm
removed distinct_fst_string;
1997-12-29, by wenzelm
improved error handling;
1997-12-28, by wenzelm
fixed execute;
1997-12-28, by wenzelm
made MLWorks happy;
1997-12-28, by wenzelm
stderr to $LOG;
1997-12-28, by wenzelm
Symtab.empty;
1997-12-28, by wenzelm
improved internal representation;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
renamed Symtab.null to Symtab.empty;
1997-12-28, by wenzelm
added >> : (theory -> theory) -> unit;
1997-12-28, by wenzelm
tuned;
1997-12-28, by wenzelm
replaced symtab.ML by table.ML;
1997-12-28, by wenzelm
renamed (is_)null to (is_)empty;
1997-12-28, by wenzelm
Generic tables (lacking delete operation). Implemented as 2-3 trees.
1997-12-27, by wenzelm
tuned;
1997-12-24, by wenzelm
export range_type;
1997-12-24, by wenzelm
improved comment;
1997-12-24, by wenzelm
More restrictive patterns to prevent changing comments
1997-12-24, by paulson
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-24, by paulson
Tidied using rev_iffD1
1997-12-23, by paulson
Now Blast_tac works properly
1997-12-23, by paulson
Tidied. Also better proof using new blast_tac
1997-12-23, by paulson
Decremented subscript because of change to iffD1
1997-12-23, by paulson
Tidied using rev_iffD1, etc
1997-12-23, by paulson
Tidied using rev_iffD1
1997-12-23, by paulson
Tidied using more default rules
1997-12-23, by paulson
Overloading info for image
1997-12-23, by paulson
tidied
1997-12-23, by paulson
New rules rev_iffD{1,2}
1997-12-23, by paulson
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-12-23, by paulson
New "obvious theorems"
1997-12-23, by paulson
Added range-type for completeness
1997-12-22, by paulson
New example
1997-12-22, by paulson
New rules rev_iffD{1,2}
1997-12-22, by paulson
corrected removal to /tmp/tmp.c
1997-12-19, by oheimb
added removal to /tmp/tmp.txt
1997-12-19, by oheimb
records without signature
1997-12-19, by narasche
remove signatrue from records
1997-12-19, by narasche
tuned;
1997-12-19, by wenzelm
new version;
1997-12-19, by wenzelm
added record.ML;
1997-12-19, by wenzelm
first version of records
1997-12-19, by narasche
pasted old insertion sort (does not work with new sort function!)
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
log file;
1997-12-19, by wenzelm
leading 0s;
1997-12-19, by wenzelm
tuned;
1997-12-19, by wenzelm
adapted to new sort function;
1997-12-19, by wenzelm
log files;
1997-12-19, by wenzelm
tuned;
1997-12-19, by wenzelm
added rev_order, make_ord;
1997-12-19, by wenzelm
term order;
1997-12-19, by wenzelm
term order stuff moved to term.ML;
1997-12-19, by wenzelm
log file;
1997-12-19, by wenzelm