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.
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
tidied
20070614, by paulson
tuned proofs: avoid implicit prems;
20070614, by wenzelm
clarified who we consider to be a contributor
20070614, by kleing
Fixed Problem with MLbindings for thm names;
20070614, by chaieb
fixed filter syntax
20070614, by nipkow
updated 'find_theorems'  moved ProofGeneral specifics to ProofGeneral/CHANGES;
20070614, by wenzelm
tuned proofs: avoid implicit prems;
20070614, by wenzelm
int abbreviates of_nat
20070613, by huffman
tuned proofs: avoid implicit prems;
20070613, by wenzelm
tuned proofs: avoid implicit prems;
20070613, by wenzelm
tuned comments;
20070613, by wenzelm
tuned proofs: avoid implicit prems;
20070613, by wenzelm
clean up instance proofs; reorganize section headings
20070613, by huffman
reactivated theory Class;
20070613, by wenzelm
added the Q_Unit rule (was missing) and adjusted the proof accordingly
20070613, by urbanc
* Isar: method "assumption" (implicit closing of subproofs) takes nonatomic goal assumptions into account;
20070613, by wenzelm
generate_fresh works even if there is no free variable in the goal
20070613, by narboux
tuned;
20070613, by wenzelm
tuned proofs: avoid implicit prems;
20070613, by wenzelm
removed constant int :: nat => int;
20070613, by huffman
thm antiquotations
20070613, by huffman
transaction: context_position (nondestructive only);
20070613, by wenzelm
added map_current;
20070613, by wenzelm
tuned msg;
20070613, by wenzelm
apply_method/end_proof: pass position;
20070613, by wenzelm
renamed map to map_current;
20070613, by wenzelm
tuned;
20070613, by wenzelm
removed unused is_atomic;
20070613, by wenzelm
renamed prove_raw to prove_internal;
20070613, by wenzelm
merge/merge_refs: plain error instead of exception TERM;
20070613, by wenzelm
Context positions.
20070613, by wenzelm
added context_position.ML;
20070613, by wenzelm
renamed Goal.prove_raw to Goal.prove_internal;
20070613, by wenzelm
Method.Basic: include position;
20070613, by wenzelm
tuned proofs: avoid implicit prems;
20070613, by wenzelm
Basic text: include position;
20070613, by wenzelm
thm antiquotations
20070612, by huffman
add lemma inj_of_nat
20070612, by huffman
thm antiquotations
20070612, by huffman
Unfortunately needed patch due to incompatibility with SML  oo is infix and hence can not appear on the left handside of patterns
20070612, by chaieb
changed int stuff into integer for SMLNJ compatibility
20070612, by chaieb
more of_rat lemmas
20070612, by huffman
add function of_rat and related lemmas
20070612, by huffman
turned curry (op opr) into curry op opr  because of smlnj
20070612, by chaieb
Deoverloaded operations for int and real.
20070612, by wenzelm
SML basis with type int representing proper integers, not machine words.
20070612, by wenzelm
Tuned proofs : now use 'algebra ad: ...'
20070612, by chaieb
cooper_tac takes now two lists of theorems to be added/deleted from the simpset dor presimplification
20070612, by chaieb
changed val restriction to local due to smlnj
20070612, by chaieb
Changed normalizer Data to contain a simpset besides the list of instances; Before the method starts, it simplifies with this simpset; Added attribute 'algebra' to add and delete theorems from the simpset above;
20070612, by chaieb
Added algebra_tac; tuned;
20070612, by chaieb
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts
20070612, by chaieb
algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts
20070612, by chaieb
less
more

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