isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
1998-03-11, by paulson
Arith.thy -> thy; proved a few new theorems
1998-03-11, by paulson
New Asm_full_simp_tac shortens proof.
1998-03-11, by nipkow
Simplifier
1998-03-11, by nipkow
More Lex.
1998-03-11, by nipkow
New Asm_full_simp_tac led to a loop.
1998-03-11, by nipkow
Mod because of new simplifier.
1998-03-10, by nipkow
Mod because of not1_or.
1998-03-10, by nipkow
Updated proofs because of new simplifier.
1998-03-10, by nipkow
Updated proofs because of new simplification tactics.
1998-03-10, by nipkow
Adapted proofs because of new simplification tactics.
1998-03-10, by nipkow
The new asm_lr_simp_tac is the old asm_full_simp_tac.
1998-03-10, by nipkow
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
1998-03-10, by oheimb
added not1_or and if_eq_cancel to simpset()
1998-03-10, by oheimb
added not1_or and if_eq_cancel to simpset()
1998-03-10, by oheimb
new rewrite rules not1_or, not2_or, and if_eq_cancel
1998-03-10, by oheimb
renamed smart_tac to force_tac, slight improvement of force_tac
1998-03-10, by oheimb
Asm_full_simp_tac now reorients asm c = t to t = c.
1998-03-10, by nipkow
adhoc fix of is_blank;
1998-03-10, by wenzelm
New scanner in abstract form.
1998-03-10, by nipkow
New simplifier flag for mutual simplification.
1998-03-10, by nipkow
Removed expand_split from simpset.
1998-03-10, by nipkow
removed pred;
1998-03-09, by wenzelm
eliminated pred function;
1998-03-09, by wenzelm
Symbol.explode;
1998-03-09, by wenzelm
replaced $LOGNAME by $USER;
1998-03-09, by wenzelm
tuned;
1998-03-09, by wenzelm
Symbol.is_*;
1998-03-09, by wenzelm
adapted to new scanner, baroque chars;
1998-03-09, by wenzelm
Symbol.input;
1998-03-09, by wenzelm
adapted to symbols, scan;
1998-03-09, by wenzelm
Generic scanners (for potentially infinite input) -- replaces Scanner;
1998-03-09, by wenzelm
adapted to new scanner and abroque chars;
1998-03-09, by wenzelm
read_var;
1998-03-09, by wenzelm
Symbol.output;
1998-03-09, by wenzelm
tuned syntax error msg;
1998-03-09, by wenzelm
Symbol.explode;
1998-03-09, by wenzelm
scan.ML, symbol.ML;
1998-03-09, by wenzelm
adapted to new scanners and baroque chars;
1998-03-09, by wenzelm
tuned some names;
1998-03-09, by wenzelm
adapted to baroque chars;
1998-03-09, by wenzelm
added merge_alists;
1998-03-09, by wenzelm
Syntax.indexname;
1998-03-09, by wenzelm
tuned comment;
1998-03-09, by wenzelm
tuned;
1998-03-09, by wenzelm
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
1998-03-09, by wenzelm
replaced Pure/Syntax/symbol_font.ML by Pure/Syntax/symbol.ML;
1998-03-09, by wenzelm
Removed `addsplits [expand_if]'
1998-03-07, by nipkow
added clasimp.ML;
1998-03-06, by wenzelm
Removed superfluous `op'
1998-03-06, by nipkow
*** empty log message ***
1998-03-06, by nipkow
Added delspilts, Addsplits, Delsplits.
1998-03-06, by nipkow
expand_if is now by default part of the simpset.
1998-03-06, by nipkow
New theorem and simprules
1998-03-05, by paulson
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Reorganized simplifier. May now reorient rules.
1998-03-04, by nipkow
Better simplification allows deletion of parts of proofs
1998-03-03, by paulson
New theorem
1998-03-03, by paulson
New theorems
1998-03-03, by paulson

less more | (0) -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle