Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
1000
300
100
60
+60
+100
+300
+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 JavaScriptenabled browsers.
Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
19960524, by nipkow
Removed junk introduced by a cvs merge.
19960524, by nipkow
Augmented comment about conversion to clauses
19960524, by paulson
expanded TABs
19960523, by berghofe
equalityI is now added to default claset
19960523, by berghofe
Removed equalityI from some proofs (because it is now included
19960523, by berghofe
Replaced fast_tac by Fast_tac (which uses default claset)
19960523, by berghofe
Added comparison with implicit rule Fun(lift s 0 @ Var 0) e> s
19960522, by nipkow
Added ex_imp
19960522, by nipkow
Added the second half of the W/I correspondence.
19960522, by nipkow
Added swap_prems_rl
19960522, by nipkow
Added additional parent theory equalities because some proofs in
19960521, by berghofe
Replaced fast_tac by Fast_tac (which uses default claset)
19960521, by berghofe
Corrected comment wrt I
19960521, by nipkow
Updated url.
19960521, by nipkow
Added thm I_complete_wrt_W to I.
19960520, by nipkow
replaced result() by qed "sorted_insort" in last proof
19960520, by berghofe
Added missing default clause  top_const _ = None;
19960517, by nipkow
Added if_image_distrib.
19960517, by nipkow
Had to rename params because variable names in an induction rule changed.
19960517, by nipkow
Moved split_rule et al from ind_syntax.ML to Prod.ML.
19960517, by nipkow
Deleted spurious line break
19960515, by paulson
Corrected and augmented timings
19960510, by paulson
Updated for new form of induction rules
19960510, by paulson
Updated for new form of induction rules
19960509, by paulson
Removed special syntax for a> and nested tuples to left
19960509, by paulson
Updated for new form of induction rules
19960509, by paulson
Added prune_params_tac to improve readability of subgoals
19960509, by paulson
moved ap_split to cartprod.ML
19960508, by paulson
Modified to use new functor signatures
19960508, by paulson
Predicates are now uncurried in both induction rules,
19960508, by paulson
Uses new ap_split from cartprod module
19960508, by paulson
New functor for operating on the two forms of Cartesian product
19960508, by paulson
Added new name cartprod
19960508, by paulson
Updated for new form of induction rules
19960508, by paulson
Updated for new form of induction rules
19960508, by paulson
Updated for new form of induction rules
19960507, by paulson
Removal of special syntax for a> and b>
19960507, by paulson
Unfolding of arbitrarily nested tuples in induction rules
19960507, by paulson
Now split_all_tac works for i>1 !
19960507, by paulson
Added function claset_of.
19960507, by berghofe
Added function for storing default claset in theory.
19960507, by berghofe
Added functions for default claset.
19960507, by berghofe
Replaced split_tac by split_inside_tac.
19960506, by berghofe
Added split_inside_tac.
19960506, by berghofe
Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
19960506, by berghofe
Updated timings; more theorems can be proved
19960506, by paulson
Now mentions but does not load mesontest2.ML
19960506, by paulson
updated comments for handling derivations
19960503, by paulson
Extra examples for safe_meson_tac
19960503, by paulson
Restored a proof of Pelletier #38  mysteriously deleted
19960502, by paulson
Added note on types.
19960502, by nipkow
Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
19960501, by paulson
New cancellation and monotonicity laws, about
19960501, by paulson
Two new "obvious" examples
19960501, by paulson
Provides merge_cs to support default clasets
19960501, by paulson
Simplified KG's proofs
19960501, by paulson
New lemma inspired by KG
19960501, by paulson
tidied some proofs
19960501, by paulson
Added an equivalence proof which avoids the use of n>
19960430, by nipkow
less
more

(0)
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip