isabelle: Graph

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

Tried to speed up the rewriter by eta-contracting all patterns beforehand and
1998-04-22, by nipkow
improved pair_tac to call prune_params_tac afterwards
1998-04-21, by oheimb
split_all_tac is now added to claset() _before_ other safe tactics
1998-04-21, by oheimb
made proof of zmult_congruent2 more stable
1998-04-21, by oheimb
simplification of explicit theory usage and merges
1998-04-21, by oheimb
removed split_all_tac from claset() globally within IOA
1998-04-21, by oheimb
made modifications of the simpset() local
1998-04-21, by oheimb
layout improvement
1998-04-21, by oheimb
expandshort; new gcd_induct with inbuilt case analysis
1998-04-21, by paulson
Renamed mod_XXX_cancel to mod_XXX_self
1998-04-21, by paulson
New laws for mod
1998-04-20, by paulson
proving fib(gcd(m,n)) = gcd(fib m, fib n)
1998-04-20, by paulson
fixed comment;
1998-04-19, by wenzelm
Fixed bug in inductive sections to allow disjunctive premises;
1998-04-10, by paulson
bug fixes
1998-04-10, by paulson
can prove the empty relation to be WF
1998-04-10, by paulson
Fixed bug in inductive sections to allow disjunctive premises;
1998-04-10, by paulson
Clearer description of recdef, including use of {}
1998-04-09, by paulson
Simplified the syntax description; mentioned FOL vs HOL
1998-04-09, by paulson
*** empty log message ***
1998-04-07, by oheimb
replaced option_map_SomeD by option_map_eq_Some (RS iffD1)
1998-04-07, by oheimb
made split_all_tac as safe wrapper more defensive:
1998-04-07, by oheimb
no open Simplifier;
1998-04-04, by wenzelm
tuned fail;
1998-04-04, by wenzelm
type_error;
1998-04-04, by wenzelm
tuned comments;
1998-04-04, by wenzelm
no open Simplifier;
1998-04-04, by wenzelm
replaced thy_data by thy_setup;
1998-04-04, by wenzelm
type_error;
1998-04-04, by wenzelm
replaced thy_data by setup;
1998-04-04, by wenzelm
removed simple;
1998-04-04, by wenzelm
added triv_goal, rev_triv_goal (for Isar);
1998-04-04, by wenzelm
added Goal_def;
1998-04-04, by wenzelm
replaced thy_data by thy_setup;
1998-04-04, by wenzelm
added local_theory (for Isar);
1998-04-04, by wenzelm
tuned trace msgs;
1998-04-04, by wenzelm
tuned names;
1998-04-03, by wenzelm
added get_tthm(s), store_tthms(s);
1998-04-03, by wenzelm
tuned comments;
1998-04-03, by wenzelm
added attribute.ML;
1998-04-03, by wenzelm
Theorem tags and attributes.
1998-04-03, by wenzelm
UNITY
1998-04-03, by paulson
repaired incompatibility with new SML version by eta-expansion
1998-04-03, by oheimb
New target HOL-UNITY
1998-04-03, by paulson
New UNITY theory
1998-04-03, by paulson
Tidied proofs
1998-04-03, by paulson
Tidied proofs by getting rid of case_tac
1998-04-03, by paulson
improved \tt appearance of many ASCII special symbols like #
1998-04-03, by oheimb
split_all_tac now fails if there is nothing to split
1998-04-02, by oheimb
new theorems
1998-04-02, by paulson
changed if_bool_eq to if_bool_eq_conj
1998-04-02, by paulson
changed if_bool_eq to if_bool_eq_conj and added if_bool_eq_disj
1998-04-02, by paulson
New theorems card_Diff_le and card_insert_le; tidied
1998-04-02, by paulson
introduced functions for updating the wrapper lists
1998-04-02, by oheimb
*** empty log message ***
1998-04-02, by oheimb
merge_cs now also merges safe and unsafe wrappers
1998-03-30, by oheimb
generalized appearance of trancl_into_rtrancl and r_into_trancl
1998-03-30, by oheimb
adapted proof of finite_converse
1998-03-30, by oheimb
added wf_converse_trancl, adapted proof of wfrec
1998-03-30, by oheimb
added caveat
1998-03-30, by oheimb
added introduction and elimination rules for Univalent
1998-03-30, by oheimb
added Univalent_rel_pow
1998-03-30, by oheimb
removed superfluous use_thy
1998-03-30, by oheimb
removed superfluous translations
1998-03-30, by oheimb
added try, single, many;
1998-03-24, by wenzelm
added cproj', and therefore extended prj
1998-03-24, by oheimb
added cproj', and therefore extended prj
1998-03-24, by oheimb
improved checks
1998-03-24, by oheimb
added o2s
1998-03-24, by oheimb
added finite_acyclic_wf_converse: corrected 8bit chars
1998-03-24, by oheimb
added acyclicI
1998-03-24, by oheimb
added finite_acyclic_wf_converse
1998-03-24, by oheimb
more thms
1998-03-23, by paulson
inverse -> converse
1998-03-16, by paulson
inverse -> converse
1998-03-16, by paulson
re-ordered proofs
1998-03-16, by paulson
moved addsplits [expand_if] from HOL_basic_ss to HOL_ss;
1998-03-13, by wenzelm
renamed not1_or to disj_not1, not2_or to disj_not2
1998-03-12, by oheimb
improved coding of delWrapper and delSWrapper
1998-03-12, by oheimb
addloop: added warning in case of overwriting a looper
1998-03-12, by oheimb
Made mutual simplification of prems a special case.
1998-03-12, by nipkow
Used merge_alists for loopers.
1998-03-12, by nipkow
New, stronger rewrites
1998-03-12, by paulson
The theorem nat_neqE, and some tidying
1998-03-12, by paulson
New laws, mostly generalizing old "pred" ones
1998-03-12, by paulson
spy_analz_tac now handles individual conjuncts properly
1998-03-11, by paulson
new theorem
1998-03-11, by paulson
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