isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

fixed comment
1998-09-11, by paulson
stabilized proof of card_mono
1998-09-11, by oheimb
corrected indentation
1998-09-11, by oheimb
equals0D
1998-09-10, by paulson
well-formed asym rules; also adds less_irrefl, le_refl since order_refl
1998-09-10, by paulson
added proof of final result...
1998-09-10, by paulson
tidied
1998-09-10, by paulson
Now WO1_WO7 has a .thy file
1998-09-10, by paulson
eliminated equals0E
1998-09-10, by paulson
fixed PROOF FAILED
1998-09-10, by paulson
tidied
1998-09-10, by paulson
deleted the bogus equals0E, fixed equals0D
1998-09-10, by paulson
eliminated equals0E
1998-09-10, by paulson
well-formed asym rules
1998-09-10, by paulson
new file AC/WO1_WO7.thy
1998-09-10, by paulson
Allows more backtracking in proof reconstruction, making it slower but more
1998-09-10, by paulson
a step to help a proof
1998-09-10, by paulson
new entries
1998-09-10, by paulson
deleted not_Says_to_self
1998-09-10, by paulson
well-formed asym rules; misc. tidying
1998-09-10, by paulson
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
1998-09-10, by paulson
tidied, fixing PROOF FAILED
1998-09-10, by paulson
tidied
1998-09-10, by paulson
tidied, eliminating hard proof
1998-09-10, by paulson
well-formed zless_asym; tidied
1998-09-10, by paulson
patch to stop failing proof
1998-09-10, by paulson
New theorem wf_not_sym and well-formed wf_asym
1998-09-10, by paulson
tided the unused rule irrefl_tranclI
1998-09-10, by paulson
Changed equals0E back to equals0D and gave it the correct destruct form
1998-09-10, by paulson
Adds order_refl, order_less_irrefl as simps, not as Iffs, to avoid PROOF FAILED
1998-09-10, by paulson
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
1998-09-10, by paulson
Proved and added rewrite rule (@x. x=y) = y to simpset.
1998-09-09, by nipkow
reflecting changes to Option.ML, List.{thy|ML}, mainly list_all
1998-09-09, by oheimb
AddIffs[not_None_eq];
1998-09-09, by oheimb
AddSDs[override_SomeD];
1998-09-09, by oheimb
changed constants mem and list_all to mere translations
1998-09-09, by oheimb
changed order of included theories
1998-09-09, by oheimb
added Id_apply
1998-09-09, by oheimb
removed superfluous AddIs thms (were already in)
1998-09-09, by oheimb
renamed sswhen to sscase
1998-09-09, by oheimb
simplified definition of axclass cpo
1998-09-09, by oheimb
added caveat; a real solution would be difficult
1998-09-08, by oheimb
improved spacing
1998-09-08, by oheimb
adapted modifiers: Mod1 -> Mod2, Mod5 -> Mod4
1998-09-08, by oheimb
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
1998-09-08, by paulson
Got rid of not_Says_to_self; re-organized proofs
1998-09-08, by paulson
new example; tidying
1998-09-07, by paulson
new example
1998-09-07, by paulson
New UNITY theory, the N-S protocol
1998-09-07, by paulson
tidying
1998-09-07, by paulson
Function 'upt'
1998-09-04, by nipkow
Arith: less_diff_conv
1998-09-04, by nipkow
A new approach, using simp_of_act and simp_of_set to activate definitions when
1998-09-03, by paulson
Added function upto to List.
1998-09-02, by nipkow
modified proofs for new constrains_tac and ensures_tac
1998-09-02, by paulson
two new thms
1998-09-02, by paulson
Moved constrains_tac from SubstAx to Constrains.
1998-09-02, by paulson
small simplification to not_Says_to_self
1998-09-02, by paulson
New approach, using a locale
1998-09-01, by paulson
tidied
1998-09-01, by paulson

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

isabelle