isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip

adapted several proofs
1996-04-23, by oheimb
*** empty log message ***
1996-04-23, by oheimb
repaired critical proofs depending on the order inside non-confluent SimpSets
1996-04-23, by oheimb
repaired critical proofs depending on the order inside non-confluent SimpSets,
1996-04-23, by oheimb
included (empty) test goal for symmetry reasons
1996-04-23, by oheimb
use_dir and exit_use_dir now change the CWD only temporarily
1996-04-23, by clasohm
inserted Suc_less_eq explictly in a few proofs.
1996-04-22, by nipkow
added Konrad's code for the datatype package
1996-04-19, by clasohm
adapted to new version of Fun.ML
1996-04-19, by clasohm
removed assignment of HOL_ss to simpset
1996-04-19, by clasohm
added thy_data.ML
1996-04-19, by clasohm
added thyname_of_sign (used in HOL/thy_data.ML)
1996-04-19, by clasohm
adapted proof of drop_succ_Cons: problem with non-confluent simpset removed
1996-04-18, by oheimb
adapted proof of less_succ: problem because of non-confluent SimpSet removed
1996-04-18, by oheimb
*** empty log message ***
1996-04-18, by oheimb
*** empty log message ***
1996-04-17, by oheimb
*** empty log message ***
1996-04-17, by oheimb
add_thydata and get_thydata now take a string as their first argument
1996-04-12, by clasohm
changed first parameter of add_thydata and get_thydata
1996-04-12, by clasohm
fixed bug in set_current_thy
1996-04-11, by clasohm
Added a number of lemmas
1996-04-11, by nipkow
select_match now sorts list of matching theorems according to the
1996-04-09, by berghofe
Replaced !simpset by HOL_ss on line 93.
1996-04-04, by nipkow
Proved Inter_0 and converse_INT
1996-04-04, by paulson

less more | (0) -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle