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 JavaScript-enabled browsers.
replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
2007-06-21, by wenzelm
Dense linear order witout endpoints
2007-06-21, by wenzelm
renamed metis-env.ML to metis_env.ML;
2007-06-21, by wenzelm
added Id;
2007-06-21, by wenzelm
fine tune automatic generation of inversion lemmas
2007-06-21, by narboux
integration of Metis prover
2007-06-21, by paulson
renamed metis-env to metis-env.ML;
2007-06-21, by wenzelm
tuned comments;
2007-06-20, by wenzelm
obsolete (cf. ATP_Linkup.thy);
2007-06-20, by wenzelm
added Tools/metis_tools.ML;
2007-06-20, by wenzelm
added Metis setup (from Metis.thy);
2007-06-20, by wenzelm
added HOL-Nominal-Examples;
2007-06-20, by wenzelm
The Metis prover (slightly modified version from Larry);
2007-06-20, by wenzelm
avoid using implicit prems in assumption
2007-06-20, by huffman
Added flexflex_first_order and tidied first_order_resolution
2007-06-20, by paulson
A more robust flexflex_unique
2007-06-20, by paulson
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
2007-06-20, by huffman
tuned error msg
2007-06-20, by krauss
Remove dedicated flag setting elements in favour of setproverflag.
2007-06-20, by aspinall
Remove dedicated flag setting elements in favour of setproverflag. Restore displayconfig response in askpgip.
2007-06-20, by aspinall
Synchronize schema with current version
2007-06-20, by aspinall
added lemmas
2007-06-20, by nipkow
added meta_impE
2007-06-20, 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
2007-06-20, by huffman
section headings
2007-06-20, by huffman
simplify some proofs
2007-06-20, by huffman
oops -- fixed profiling;
2007-06-19, by wenzelm
Balanced binary trees (material from library.ML);
2007-06-19, by wenzelm
profiling: observe no_timing;
2007-06-19, by wenzelm
added raw_tactic;
2007-06-19, by wenzelm
moved balanced tree operations to General/balanced_tree.ML;
2007-06-19, by wenzelm
added with_subgoal;
2007-06-19, by wenzelm
balanced conjunctions;
2007-06-19, by wenzelm
balanced conjunctions;
2007-06-19, by wenzelm
added General/balanced_tree.ML;
2007-06-19, by wenzelm
BalancedTree;
2007-06-19, by wenzelm
balanced conjunctions;
2007-06-19, by wenzelm
tuned;
2007-06-19, by wenzelm
generalized proofs so that call graphs can have any node type.
2007-06-19, by krauss
macbroy5: trying -j 2;
2007-06-19, by wenzelm
tuned conjunction tactics: slightly smaller proof terms;
2007-06-18, by wenzelm
tuned laws for cancellation in divisions for fields.
2007-06-17, by nipkow
moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs
2007-06-17, by chaieb
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl
2007-06-17, by chaieb
gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;
2007-06-17, by chaieb
thin_prems_tac first max-scopes universal quantifiers; eta_conv moved to Pure/conv.ML
2007-06-17, by chaieb
Tuned error messages; tuned;
2007-06-17, by chaieb
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
2007-06-17, by chaieb
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
2007-06-17, by chaieb
moved lemma all_not_ex to HOL.thy ; tuned proofs
2007-06-17, by chaieb
Tuned instantiation of Groebner bases to fields
2007-06-17, by chaieb
added Theorem all_not_ex
2007-06-17, by chaieb
renamed vars in zle_trans for compatibility
2007-06-17, by nipkow
tuned
2007-06-16, by nipkow
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
2007-06-16, by nipkow
Locally added definition of "int :: nat => int" again to make
2007-06-15, by berghofe
made divide_self a simp rule
2007-06-15, by nipkow
Removed thunk from Fun
2007-06-15, by nipkow
Church numerals added
2007-06-15, by nipkow
method assumption: uniform treatment of prems as legacy feature;
2007-06-14, by wenzelm
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip