Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-1000
-120
+120
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
Classical tactics now use default claset.
1996-06-21, by berghofe
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
1996-06-21, by oheimb
Restored Addsimps [Suc_le_lessD], as it cannot be added
1996-06-20, by paulson
Corrected comment
1996-06-20, by paulson
New rewrites for vacuous quantification
1996-06-18, by paulson
Addition of setOfList
1996-06-18, by paulson
Addition of Safe_step_tac
1996-06-18, by paulson
Translation infixes <->, etc., no longer available at top-level
1996-06-18, by paulson
Addition of setOfList
1996-06-18, by paulson
Removal of list_all
1996-06-18, by paulson
Translation infixes <->, etc., no longer available at top-level
1996-06-18, by paulson
Inserted comment about problem 43
1996-06-17, by paulson
Removed quantification over lists
1996-06-17, by paulson
Now exports Delrules
1996-06-17, by paulson
Converted to use constdefs instead of defs
1996-06-17, by paulson
Explicitly included add_mult_distrib & add_mult_distrib2
1996-06-14, by paulson
New example of greatest common divisor
1996-06-14, by paulson
Added Primes to list of theories in target ex
1996-06-14, by paulson
Now del_simp catches the right exception!
1996-06-14, by paulson
Added delete function for brls
1996-06-14, by paulson
Now implements delrules
1996-06-14, by paulson
Added new Primes theory
1996-06-14, by paulson
Explicitly included add_mult_distrib & add_mult_distrib2
1996-06-14, by paulson
Updated list of theories for target ex
1996-06-14, by paulson
Tidied spacing
1996-06-14, by paulson
New lemmas for gcd example
1996-06-14, by paulson
Obsolete relics concerned with recursion
1996-06-14, by paulson
New example of GCDs and divides relation
1996-06-13, by paulson
The "divides" relation, the greatest common divisor and Euclid's algorithm
1996-06-13, by paulson
Addition of converse_iff, domain_converse, range_converse as rewrites
1996-06-07, by paulson
Quotes now optional around inductive set
1996-06-06, by paulson
Quotes now optional around inductive set
1996-06-06, by paulson
Quotes now optional around inductive set
1996-06-06, by paulson
Tidied some proofs
1996-06-04, by paulson
best_tac, deepen_tac and safe_tac now also use default claset.
1996-06-03, by berghofe
Shortened some proofs
1996-06-03, by paulson
Added a new theorem, UN_Int_subset
1996-06-03, by paulson
Used 2 instead of Suc(Suc 0)
1996-06-03, by paulson
Shortened a proof
1996-06-03, by paulson
adapted use of monofun_cfun_arg
1996-05-31, by oheimb
adapted proof of flat_codom
1996-05-31, by oheimb
introduced forgotten bind_thm calls
1996-05-31, by oheimb
adapted some proofs for new simplifier
1996-05-31, by oheimb
renamed le_0 to le_0_eq, to avoid confusion with le0,
1996-05-31, by oheimb
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
1996-05-31, by oheimb
Smaller logo
1996-05-30, by nipkow
Regrouped logo
1996-05-30, by nipkow
Added logo
1996-05-29, by nipkow
An Isabelle logo
1996-05-29, by nipkow
Replaced setsolver by addsolver
1996-05-29, by nipkow
Added addsolver
1996-05-29, by nipkow
Simplified proof of deduction theorem
1996-05-28, by paulson
Corrected a comment in #34
1996-05-28, by paulson
Rules pred_0, pred_Suc etc. are now stored in theorem database.
1996-05-24, by berghofe
Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
1996-05-24, by nipkow
Removed junk introduced by a cvs merge.
1996-05-24, by nipkow
Augmented comment about conversion to clauses
1996-05-24, by paulson
expanded TABs
1996-05-23, by berghofe
equalityI is now added to default claset
1996-05-23, by berghofe
Removed equalityI from some proofs (because it is now included
1996-05-23, by berghofe
Replaced fast_tac by Fast_tac (which uses default claset)
1996-05-23, by berghofe
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
1996-05-22, by nipkow
Added ex_imp
1996-05-22, by nipkow
Added the second half of the W/I correspondence.
1996-05-22, by nipkow
Added swap_prems_rl
1996-05-22, by nipkow
Added additional parent theory equalities because some proofs in
1996-05-21, by berghofe
Replaced fast_tac by Fast_tac (which uses default claset)
1996-05-21, by berghofe
Corrected comment wrt I
1996-05-21, by nipkow
Updated url.
1996-05-21, by nipkow
Added thm I_complete_wrt_W to I.
1996-05-20, by nipkow
replaced result() by qed "sorted_insort" in last proof
1996-05-20, by berghofe
Added missing default clause | top_const _ = None;
1996-05-17, by nipkow
Added if_image_distrib.
1996-05-17, by nipkow
Had to rename params because variable names in an induction rule changed.
1996-05-17, by nipkow
Moved split_rule et al from ind_syntax.ML to Prod.ML.
1996-05-17, by nipkow
Deleted spurious line break
1996-05-15, by paulson
Corrected and augmented timings
1996-05-10, by paulson
Updated for new form of induction rules
1996-05-10, by paulson
Updated for new form of induction rules
1996-05-09, by paulson
Removed special syntax for -a-> and nested tuples to left
1996-05-09, by paulson
Updated for new form of induction rules
1996-05-09, by paulson
Added prune_params_tac to improve readability of subgoals
1996-05-09, by paulson
moved ap_split to cartprod.ML
1996-05-08, by paulson
Modified to use new functor signatures
1996-05-08, by paulson
Predicates are now uncurried in both induction rules,
1996-05-08, by paulson
Uses new ap_split from cartprod module
1996-05-08, by paulson
New functor for operating on the two forms of Cartesian product
1996-05-08, by paulson
Added new name cartprod
1996-05-08, by paulson
Updated for new form of induction rules
1996-05-08, by paulson
Updated for new form of induction rules
1996-05-08, by paulson
Updated for new form of induction rules
1996-05-07, by paulson
Removal of special syntax for -a-> and -b->
1996-05-07, by paulson
Unfolding of arbitrarily nested tuples in induction rules
1996-05-07, by paulson
Now split_all_tac works for i>1 !
1996-05-07, by paulson
Added function claset_of.
1996-05-07, by berghofe
Added function for storing default claset in theory.
1996-05-07, by berghofe
Added functions for default claset.
1996-05-07, by berghofe
Replaced split_tac by split_inside_tac.
1996-05-06, by berghofe
Added split_inside_tac.
1996-05-06, by berghofe
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
1996-05-06, by berghofe
Updated timings; more theorems can be proved
1996-05-06, by paulson
Now mentions but does not load mesontest2.ML
1996-05-06, by paulson
updated comments for handling derivations
1996-05-03, by paulson
Extra examples for safe_meson_tac
1996-05-03, by paulson
Restored a proof of Pelletier #38 -- mysteriously deleted
1996-05-02, by paulson
Added note on types.
1996-05-02, by nipkow
Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
1996-05-01, by paulson
New cancellation and monotonicity laws, about
1996-05-01, by paulson
Two new "obvious" examples
1996-05-01, by paulson
Provides merge_cs to support default clasets
1996-05-01, by paulson
Simplified KG's proofs
1996-05-01, by paulson
New lemma inspired by KG
1996-05-01, by paulson
tidied some proofs
1996-05-01, by paulson
Added an equivalence proof which avoids the use of -n->
1996-04-30, by nipkow
Added backwards rtrancl_induct and special versions for pairs.
1996-04-30, by nipkow
changed ident_no_colon so that it forbids postfix "=", too
1996-04-30, by clasohm
changed use_thy's behaviour so that if the user specifies a path for a theory
1996-04-30, by clasohm
moved dest_cimplies to drule.ML; added adjust_maxidx
1996-04-30, by clasohm
Cosmetic re-ordering of declarations
1996-04-30, by paulson
Streamlined syntax: -(n)-> is now -n->.
1996-04-29, by nipkow
less
more
|
(0)
-1000
-120
+120
+1000
+3000
+10000
+30000
tip