Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
3000
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.
added Metis setup (from Metis.thy);
20070620, by wenzelm
added HOLNominalExamples;
20070620, by wenzelm
The Metis prover (slightly modified version from Larry);
20070620, by wenzelm
avoid using implicit prems in assumption
20070620, by huffman
Added flexflex_first_order and tidied first_order_resolution
20070620, by paulson
A more robust flexflex_unique
20070620, by paulson
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
20070620, by huffman
tuned error msg
20070620, by krauss
Remove dedicated flag setting elements in favour of setproverflag.
20070620, by aspinall
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
20070620, by aspinall
Synchronize schema with current version
20070620, by aspinall
added lemmas
20070620, by nipkow
added meta_impE
20070620, by nipkow
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
20070620, by huffman
section headings
20070620, by huffman
simplify some proofs
20070620, by huffman
oops  fixed profiling;
20070619, by wenzelm
Balanced binary trees (material from library.ML);
20070619, by wenzelm
profiling: observe no_timing;
20070619, by wenzelm
added raw_tactic;
20070619, by wenzelm
moved balanced tree operations to General/balanced_tree.ML;
20070619, by wenzelm
added with_subgoal;
20070619, by wenzelm
balanced conjunctions;
20070619, by wenzelm
balanced conjunctions;
20070619, by wenzelm
added General/balanced_tree.ML;
20070619, by wenzelm
BalancedTree;
20070619, by wenzelm
balanced conjunctions;
20070619, by wenzelm
tuned;
20070619, by wenzelm
generalized proofs so that call graphs can have any node type.
20070619, by krauss
macbroy5: trying j 2;
20070619, by wenzelm
tuned conjunction tactics: slightly smaller proof terms;
20070618, by wenzelm
tuned laws for cancellation in divisions for fields.
20070617, by nipkow
moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs
20070617, by chaieb
Added eta_conv and etaexpansion conversion: waiting for it to be in thm.ML; exported is_refl
20070617, by chaieb
gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for etacontracted f;
20070617, by chaieb
thin_prems_tac first maxscopes universal quantifiers; eta_conv moved to Pure/conv.ML
20070617, by chaieb
Tuned error messages; tuned;
20070617, by chaieb
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
20070617, by chaieb
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
20070617, by chaieb
moved lemma all_not_ex to HOL.thy ; tuned proofs
20070617, by chaieb
Tuned instantiation of Groebner bases to fields
20070617, by chaieb
added Theorem all_not_ex
20070617, by chaieb
renamed vars in zle_trans for compatibility
20070617, by nipkow
tuned
20070616, by nipkow
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
20070616, by nipkow
Locally added definition of "int :: nat => int" again to make
20070615, by berghofe
made divide_self a simp rule
20070615, by nipkow
Removed thunk from Fun
20070615, by nipkow
Church numerals added
20070615, by nipkow
method assumption: uniform treatment of prems as legacy feature;
20070614, by wenzelm
tuned proofs;
20070614, by wenzelm
tuned proofs: avoid implicit prems;
20070614, by wenzelm
fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other)
20070614, by chaieb
no computation rules in the presimplifiaction set
20070614, by chaieb
Added some lemmas to default presburger simpset; tuned proofs
20070614, by chaieb
tuned proofs: avoid implicit prems;
20070614, by wenzelm
tuned proofs: avoid implicit prems;
20070614, by wenzelm
Now ResHolClause also does firstorder problems!
20070614, by paulson
Now also handles FO problems
20070614, by paulson
Deleted unused code
20070614, by paulson
less
more

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