isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

Optimized version of SELECT_GOAL, up to 10% faster
1996-09-23, by paulson
New operations on cterms. Now same names as in Logic
1996-09-23, by paulson
Addition of gensym
1996-09-23, by paulson
Bad version of Otway-Rees and the new attack on it
1996-09-23, by paulson
Reformatting; proved B_gets_secure_key
1996-09-13, by paulson
Abstraction of enemy_analz_tac over its argument
1996-09-13, by paulson
Reformatting
1996-09-13, by paulson
Reordering of premises for cut theorems, and new law MPair_synth_analz
1996-09-13, by paulson
No longer assumes Alice is not the Enemy in NS3.
1996-09-13, by paulson
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
1996-09-13, by paulson
Addition of Yahalom protocol
1996-09-13, by paulson
Removal of obsolete thm Fake_parts_insert
1996-09-13, by paulson
Addition of enemy_analz_tac and safe_solver
1996-09-13, by paulson
added flat_eq,
1996-09-12, by oheimb
renamed adm_disj_lemma11 to adm_lemma11
1996-09-12, by oheimb
added comment on is_flat
1996-09-12, by oheimb
added stric
1996-09-12, by oheimb
undo last revision
1996-09-12, by oheimb
bin/isa2latex: copy the binary to bin/isa2latex instead of linking it there
1996-09-12, by oheimb
new \subsubsection{Configuring conversion tables and keyboard bindings}
1996-09-12, by oheimb
Tidied many proofs, using AddIffs to let equivalences take
1996-09-12, by paulson
Installed AddIffs, and some code from HOL.ML
1996-09-12, by paulson
Simplification and tidying of definitions
1996-09-12, by paulson
Now hologic.ML is loaded in HOL.ML
1996-09-12, by paulson
New file cladata.ML
1996-09-12, by paulson
Split off classical reasoning code to cladata.ML
1996-09-12, by paulson
Change to best_tac required to prevent looping
1996-09-12, by paulson
Moved RSLIST here from ../Relation.ML
1996-09-11, by paulson
Removal of univ_cs
1996-09-11, by paulson
Reformatting
1996-09-11, by paulson
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
1996-09-11, by nipkow
Removed refs to clasets like rel_cs etc. Used implicit claset.
1996-09-11, by nipkow
Converted proofs to use default clasets.
1996-09-10, by nipkow
Added Auth to the test target
1996-09-10, by paulson
Now runs all Auth proofs
1996-09-10, by paulson
Now uses DB-ROOT.ML, which is separate from ROOT.ML
1996-09-10, by paulson
Dedicated root file for making the Auth database
1996-09-10, by paulson
Beefed-up auto-tactic: now repeatedly simplifies if needed
1996-09-10, by paulson
"bad" set simplifies statements of many theorems
1996-09-09, by paulson
added cterm_lift_inst_rule
1996-09-09, by nipkow
Stronger proofs; work for Otway-Rees
1996-09-09, by paulson
Stronger proofs; work for Otway-Rees
1996-09-09, by paulson
These simpsets must not use miniscoping
1996-09-09, by paulson
Corrected associativity: must be to right, as the type dictatess
1996-09-09, by paulson
Removal of (EX x. P) <-> P and (ALL x. P) <-> P
1996-09-09, by paulson
Improved error handling: if there are syntax or type-checking
1996-09-06, by paulson
Modified proof to work with miniscoping
1996-09-06, by paulson
Now uses thin_tac
1996-09-05, by paulson
Now uses thin_tac
1996-09-05, by paulson
Renaming of _rews to _simps
1996-09-05, by paulson
Added thin_tac to signature; previous change was useless
1996-09-05, by paulson
Some renaming. Note that this miniscoping is more
1996-09-05, by paulson
Introduction of miniscoping for FOL
1996-09-05, by paulson
Pretty-printing change to emphasize the scope of assumptions
1996-09-05, by paulson
Declared thin_tac
1996-09-05, by paulson
Miniscoping rules are deleted, as these brittle proofs
1996-09-05, by paulson
Simplified some proofs for compatibility with miniscoping
1996-09-05, by paulson
Added miniscoping to the simplifier: quantifiers are now pushed in
1996-09-05, by paulson
Fixed pretty-printing of {|...|}
1996-09-03, by paulson
New theorems for Fake case
1996-09-03, by paulson

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

isabelle