isabelle: Graph

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

converted many HOL/Auth theories to Isar scripts
2001-04-12, by paulson
symlinks to ../../../HOL/Auth. Fingers crossed...
2001-04-11, by paulson
Protocols chapter
2001-04-10, by paulson
back to Unix format...
2001-04-10, by paulson
security protocol chapter
2001-04-10, by paulson
security protocol refs
2001-04-10, by paulson
new theorem Fake_parts_insert_in_Un
2001-04-09, by paulson
extra display
2001-04-09, by paulson
*** empty log message ***
2001-04-09, by paulson
lexicographic product of two relations: updated HOL.tex
2001-04-09, by paulson
Isar hint
2001-04-09, by paulson
thm output: Attrib.local_thmss;
2001-04-07, by wenzelm
tuned
2001-04-07, by wenzelm
*** empty log message ***
2001-03-30, by nipkow
*** empty log message ***
2001-03-30, by nipkow
*** empty log message ***
2001-03-30, by nipkow
*** empty log message ***
2001-03-30, by nipkow
quantifier instantiation
2001-03-30, by paulson
the one-point rule for bounded quantifiers
2001-03-30, by paulson
generalization of 1 point rules for ALL
2001-03-29, by nipkow
*** empty log message ***
2001-03-29, by nipkow
misc tidying; changing the predicate isSymKey to the set symKeys
2001-03-29, by paulson
Got rid of is_dfa
2001-03-28, by nipkow
MicroJava/BV dependencies incomplete
2001-03-28, by nipkow
fixed bug in tactic for ball 1 point simproc
2001-03-27, by nipkow
Vos
2001-03-27, by paulson
simplified proofs
2001-03-26, by nipkow
simplified proofs
2001-03-26, by nipkow
I forgot a few bases cases for the 1-point rules...
2001-03-26, by nipkow
shortening and streamlining of proofs
2001-03-23, by paulson
added simproc for bounded quantifiers
2001-03-23, by nipkow
added one point simprocs for bounded quantifiers
2001-03-23, by nipkow
new theorem analz_Decrypt'
2001-03-22, by paulson
new theorem analz_isSymKey_Decrypt
2001-03-22, by paulson
some X-symbols
2001-03-22, by paulson
*** empty log message ***
2001-03-19, by nipkow
*** empty log message ***
2001-03-19, by nipkow
*** empty log message ***
2001-03-19, by nipkow
*** empty log message ***
2001-03-19, by nipkow
*** empty log message ***
2001-03-19, by paulson
translations: a tweak
2001-03-15, by paulson
*** empty log message ***
2001-03-15, by nipkow
*** empty log message ***
2001-03-15, by nipkow
*** empty log message ***
2001-03-15, by nipkow
*** empty log message ***
2001-03-15, by nipkow
*** empty log message ***
2001-03-14, by nipkow
*** empty log message ***
2001-03-14, by nipkow
minor tuning
2001-03-14, by paulson
*** empty log message ***
2001-03-13, by nipkow
*** empty log message ***
2001-03-12, by nipkow
*** empty log message ***
2001-03-12, by nipkow
arith_tac now copes with propositional reasoning as well.
2001-03-09, by nipkow
expanded abbrevs
2001-03-07, by paulson
added strange 'b y' syntax
2001-03-07, by streckem
*** empty log message ***
2001-03-07, by nipkow
*** empty log message ***
2001-03-07, by nipkow
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
2001-03-05, by paulson
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
2001-03-05, by paulson
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
2001-03-05, by paulson
a few basic X-symbols
2001-03-05, by paulson
conversion of Message.thy to Isar format
2001-03-02, by paulson
*** empty log message ***
2001-03-02, by ehmety
conversion of Message.thy to Isar format
2001-03-02, by paulson
streamlined a proof
2001-03-02, by paulson
auto-update
2001-02-28, by paulson
*** empty log message ***
2001-02-27, by nipkow
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
2001-02-27, by paulson
kildall now via while and therefore executable!
2001-02-27, by nipkow
minor tweaks to speed the proofs
2001-02-26, by paulson
minor fixes
2001-02-26, by paulson
renamed addaltern to addafter, addSaltern to addSafter
2001-02-23, by oheimb
removed performance leak for split_conv_tac (and corresponding safe wrapper)
2001-02-23, by oheimb
subst method and a new section on rule, rule_tac, etc
2001-02-22, by paulson
removed unused constant
2001-02-22, by kleing
removed unused function
2001-02-22, by kleing
a PROPER tidy-up
2001-02-22, by paulson
recoded function iter with the help of the while-combinator.
2001-02-22, by nipkow
revisions in response to comments by Tobias
2001-02-21, by paulson
revisions in response to comments by Tobias
2001-02-21, by paulson
added split_conv_tac (also to claset()) as an optimization
2001-02-21, by oheimb
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
2001-02-20, by oheimb
simplified proofs for splitI and splitD, added splitD'
2001-02-20, by oheimb
made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
2001-02-20, by oheimb
corrected comments on addbefore and addSbefore
2001-02-20, by oheimb
added same_fstI
2001-02-20, by oheimb
simplified definition of wrapper bspec
2001-02-20, by oheimb
added image_cong to default congs of recdef
2001-02-20, by oheimb
added add_arith (just as hint by now)
2001-02-20, by oheimb
added rearrange_prems
2001-02-20, by oheimb
debugging: replaced gen_all by forall_elim_vars_safe
2001-02-20, by oheimb
*** empty log message ***
2001-02-20, by nipkow
*** empty log message ***
2001-02-20, by nipkow
*** empty log message ***
2001-02-20, by nipkow
*** empty log message ***
2001-02-20, by nipkow
*** empty log message ***
2001-02-17, by nipkow
fixed the obvious errors Tobias found
2001-02-16, by paulson
Least_def now refers to LeastM
2001-02-16, by paulson
for the change to LEAST
2001-02-16, by paulson
Blast bug fix made old proof too slow
2001-02-16, by paulson
Blast bug fix: now always duplicates when applying a haz rule,
2001-02-16, by paulson
Blast bug fix made old proof too slow
2001-02-16, by paulson
Streamlining for the bug fix in Blast.
2001-02-16, by paulson
*** empty log message ***
2001-02-16, by nipkow
*** empty log message ***
2001-02-16, by nipkow
*** empty log message ***
2001-02-16, by nipkow
tuned;
2001-02-16, by wenzelm
eliminate get_def; Isabelle99-2
2001-02-15, by wenzelm
tuned;
2001-02-15, by wenzelm
Ord.thy/.ML converted to Isar
2001-02-15, by oheimb
moved inv_image to Relation
2001-02-15, by oheimb
supressed some warnings on identical proofstate
2001-02-15, by oheimb
Ord.thy/.ML converted to Isar
2001-02-15, by oheimb
moved wellorder_LeastI,wellorder_Least_le,wellorder_not_less_Least
2001-02-15, by oheimb
simplified proof of Least_mono
2001-02-15, by oheimb
added wellorder axclass
2001-02-15, by oheimb
moved inv_image to Relation
2001-02-15, by oheimb
moved wf_less from Nat.ML to NatDef.ML
2001-02-15, by oheimb
added nat as instance of new wellorder axclass
2001-02-15, by oheimb
Ord.thy/.ML converted to Isar
2001-02-15, by oheimb
added trial proof
2001-02-15, by oheimb