Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-3000
-1000
-240
+240
+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 JavaScript-enabled browsers.
Replaced "init_thy_reader" by "set_parser".
1997-08-06, by berghofe
Removed reference to "thy_data.ML".
1997-08-06, by berghofe
The functions in this file have been moved to "cladata.ML"
1997-08-06, by berghofe
Moved functions from file "thy_data.ML".
1997-08-06, by berghofe
Replaced "init_thy_reader" by "set_parser".
1997-08-06, by berghofe
Replaced "init_thy_reader" by set_parser.
1997-08-06, by berghofe
Added some new dependencies for files in subdirectory Thy.
1997-08-06, by berghofe
Added function "file_exists".
1997-08-06, by berghofe
Removed function file_exists (now included in library.ML)
1997-08-06, by berghofe
Moved functions for theory information storage / retrieval
1997-08-06, by berghofe
This file now contains all functions for generating html
1997-08-06, by berghofe
Moved several functions:
1997-08-06, by berghofe
Moved "qed" - functions etc. from thy_read.ML to thm_database.ML.
1997-08-06, by berghofe
Added some additional "use" commands for new files
1997-08-06, by berghofe
Source files for Isabelle theory graph browser.
1997-08-06, by berghofe
Makefile for GraphBrowser
1997-08-06, by berghofe
added getenv;
1997-08-05, by wenzelm
removed smlnj-1.07;
1997-08-05, by wenzelm
cleaned up;
1997-08-05, by wenzelm
tuned comments;
1997-08-05, by wenzelm
removed ML-Systems/smlnj-1.07.ML;
1997-08-05, by wenzelm
SML/NJ 1.07 no longer supported!
1997-08-05, by wenzelm
cleaned up;
1997-08-05, by wenzelm
Added example mapf which requires a special congruence rule.
1997-08-05, by nipkow
Added function `replicate' and lemmas map_cong and set_replicate.
1997-08-05, by nipkow
cleaned up;
1997-08-05, by wenzelm
Corrected a comment
1997-08-05, by paulson
Added a take/dropWhile lemma.
1997-08-04, by nipkow
Generalized nth_drop (Conny).
1997-08-01, by nipkow
Corected bug in def of dropWhile (also present in Haskell lib!)
1997-08-01, by nipkow
Had to remove {x.x=a} = a from !simpset in one proof.
1997-08-01, by nipkow
Added {x.x=a} = a to !simpset.
1997-08-01, by nipkow
removed split_paired_Ex;
1997-07-25, by wenzelm
new simproc
1997-07-25, by nipkow
*** empty log message ***
1997-07-25, by wenzelm
load simplifier.ML (again);
1997-07-25, by wenzelm
added prems argument to simplification procedures;
1997-07-25, by wenzelm
remove references to simplifier.ML;
1997-07-25, by wenzelm
improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-25, by wenzelm
Added a few lemmas.
1997-07-24, by nipkow
Deleted comment.
1997-07-24, by nipkow
Replaced clumsy rewriting by the new function simplify on thms.
1997-07-24, by nipkow
List.ML: added lemmas by Stefan Merz.
1997-07-24, by nipkow
set_of_list -> set
1997-07-24, by paulson
Simplified a few proofs because of improved simplification.
1997-07-23, by nipkow
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
1997-07-23, by nipkow
added simplification meta rules;
1997-07-23, by wenzelm
standard congs;
1997-07-23, by wenzelm
Now rename_params_rule merely issues warnings--and does nothing--if the
1997-07-23, by paulson
Now Datatype.occs_in_prems prints the necessary warning ITSELF.
1997-07-23, by paulson
Uses new version of Datatype.occs_in_prems
1997-07-23, by paulson
auto update
1997-07-23, by paulson
Removal of tactical STATE
1997-07-23, by paulson
fixed polymorphic val;
1997-07-23, by wenzelm
tuned congs: standard;
1997-07-23, by wenzelm
improved simp tracing;
1997-07-23, by wenzelm
added simplification meta rules;
1997-07-23, by wenzelm
tmp fix to accomodate rep_ss changes;
1997-07-23, by wenzelm
added rewrite_thm;
1997-07-23, by wenzelm
tuned apsome;
1997-07-23, by wenzelm
added error_msg;
1997-07-22, by wenzelm
tuned error / warning;
1997-07-22, by wenzelm
added print_ss;
1997-07-22, by wenzelm
added dest_mss, merge_mss;
1997-07-22, by wenzelm
tuned title;
1997-07-22, by wenzelm
added dest and merge operations;
1997-07-22, by wenzelm
added pretty_cterm;
1997-07-22, by wenzelm
improved print_cs;
1997-07-22, by wenzelm
Cosmetic changes: margins, indentation, ...
1997-07-22, by paulson
Now possibility_tac is an explicit function, in order to delay
1997-07-22, by paulson
Cosmetic changes: margins, indentation, ...
1997-07-22, by paulson
Now possibility_tac and basic_possibility_tac are explicit functions, in order
1997-07-22, by paulson
Deleted the superfluous assumption A ~= B, which must hold anyway by induction
1997-07-22, by paulson
Fixed the spelling of AUTH_NAMES--it could not have worked before\!
1997-07-22, by paulson
Option is a synonym for General because MLWorks does not yet provide
1997-07-22, by paulson
Removal of the tactical STATE
1997-07-22, by paulson
Removal of the tactical STATE
1997-07-22, by paulson
tuned error propagation msg;
1997-07-18, by wenzelm
defs may now be conditional;
1997-07-18, by wenzelm
renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
tuned warnings;
1997-07-18, by wenzelm
considered removal of print_goals_ref;
1997-07-18, by wenzelm
defs: allow conditions;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
renamed |-> <-| <-> to Parse/PrintRule;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
tuned warning;
1997-07-18, by wenzelm
improved output channels: normal, warning, error;
1997-07-18, by wenzelm
fixed EqI meta rule;
1997-07-17, by wenzelm
changes needed for introducing fairness
1997-07-17, by mueller
changes neede for introducing fairness
1997-07-17, by mueller
changes needed for adding fairness
1997-07-17, by mueller
fixed merge of internal simprocs;
1997-07-16, by wenzelm
Changing "lost" from a parameter of protocol definitions to a constant.
1997-07-14, by paulson
Fixed delIffs to deal correctly with the D-rule
1997-07-14, by paulson
Removed redundant addsimps of Un_insert_left, which is now a default simprule
1997-07-14, by paulson
Removal of monotonicity reasoning involving "lost" and the theorem
1997-07-11, by paulson
Now uses the Notes constructor to distinguish the Client (who has chosen M)
1997-07-11, by paulson
Moved some declarations to Message from Public and Shared
1997-07-11, by paulson
Now loads theory Event, which contains common declarations
1997-07-11, by paulson
Moving common declarations and proofs from theories "Shared"
1997-07-11, by paulson
removed obsolete init_pps and init_thy_reader;
1997-07-09, by wenzelm
improved type checking errors;
1997-07-09, by wenzelm
removed init_pps;
1997-07-09, by wenzelm
removed init_database;
1997-07-09, by wenzelm
Improved length = size translation.
1997-07-09, by nipkow
New proofs involving CERTIFICATE VERIFY
1997-07-07, by paulson
eliminated chmod -w;
1997-07-07, by wenzelm
-w option;
1997-07-07, by wenzelm
NOWRITE;
1997-07-07, by wenzelm
added -w option;
1997-07-07, by wenzelm
Changed some variables of type msg to lower case (e.g. from NB to nb
1997-07-04, by paulson
New constant "certificate"--just an abbreviation
1997-07-04, by paulson
Reduced priority of postfix ^* etc operators such that they are the same as
1997-07-04, by nipkow
Automatic update
1997-07-04, by paulson
Now catches the error of calling tgoalw when there are no goals to prove,
1997-07-04, by paulson
Simplified the new proofs about division
1997-07-04, by paulson
New comments on how to deal with unproved termination conditions
1997-07-04, by paulson
Fixed comments
1997-07-04, by paulson
Moved MLWorks.ML to its proper place, directory ML-Systems.
1997-07-04, by paulson
Automatic update
1997-07-04, by paulson
Modified the \tydx command to set types in italics instead of \tt
1997-07-03, by paulson
Some LaTeX-2e primitives such as \texttt
1997-07-03, by paulson
Added documentation for recdef, and tidied some other material
1997-07-03, by paulson
Updated references
1997-07-03, by paulson
set_of_list -> set
1997-07-03, by nipkow
Now there are TWO spaces after each full stop, so that the Emacs sentence
1997-07-02, by paulson
Now there are TWO spaces after each full stop, so that the Emacs sentence
1997-07-02, by paulson
Added the following lemmas tp Divides and a few others to Arith and NatDef:
1997-07-02, by nipkow
Tidying; also simplified the lemma Says_Server_not
1997-07-01, by paulson
New theory TLS
1997-07-01, by paulson
Deleted a redundant A~=B in rules that refer to a previous event
1997-07-01, by paulson
More realistic model: the Spy can compute clientK and serverK
1997-07-01, by paulson
Reordered rules in analz_image_freshK_ss to improve clarity
1997-07-01, by paulson
Removal of the obsolete newN function
1997-07-01, by paulson
New theorem priK_inj_eq, injectivity of priK
1997-07-01, by paulson
spy_analz_tac: Restored iffI to the list of rules used to break down
1997-07-01, by paulson
New theory TLS
1997-07-01, by paulson
Baby TLS. Proofs work, but model seems unrealistic
1997-07-01, by paulson
New and stronger lemmas; more default simp/cla rules
1997-07-01, by paulson
Deleted the obsolete operators newK, newN and nPair
1997-07-01, by paulson
Now the possibility proof calls the appropriate tactic
1997-07-01, by paulson
Added a comment
1997-07-01, by paulson
Now Collect_mem_eq is a default simprule (how could it have ever been omitted?
1997-07-01, by paulson
New laws for the "lists" operator
1997-07-01, by paulson
More concat lemmas.
1997-06-30, by nipkow
Corrected indentations and margins after the renaming of "set_of_list"
1997-06-27, by paulson
set_of_list -> set
1997-06-26, by nipkow
Trivial changes in connection with the Yahalom paper.
1997-06-26, by paulson
oops;
1997-06-26, by wenzelm
rearrange pages of ps file to be printed as booklet (duplex);
1997-06-26, by wenzelm
amdI -> admI2
1997-06-26, by nipkow
Tuned Franz's proofs.
1997-06-26, by nipkow
Removal of structure Context and its replacement by a theorem list of
1997-06-23, by paulson
Removal of COND_CONG, which is just if_cong RS eq_reflection
1997-06-23, by paulson
Ran expandshort
1997-06-23, by paulson
New "congs" keyword for recdef theory section
1997-06-23, by paulson
removed old Makefile;
1997-06-20, by wenzelm
removed;
1997-06-20, by wenzelm
removed old Makefile;
1997-06-20, by wenzelm
removed old Makefile and compat files;
1997-06-20, by wenzelm
Made proofs more concise by replacing calls to spy_analz_tac by uses of
1997-06-19, by paulson
Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
1997-06-19, by paulson
New comments; a tidied proof
1997-06-19, by paulson
Two new rewrite rules--NOT included by default\!
1997-06-19, by paulson
Defines KeyWithNonce, which is used to prove the secrecy of NB
1997-06-18, by paulson
Addition of not_imp (which pushes negation into implication) as a default
1997-06-18, by paulson
Corrected Title in header lines
1997-06-18, by paulson
Streamlined proofs of the secrecy of NB and added authentication of A and B
1997-06-18, by paulson
Removed Says_Crypt_lost and Says_Crypt_not_lost.
1997-06-18, by paulson
Removed Says_Crypt_lost and Says_Crypt_not_lost.
1997-06-18, by paulson
Adapted proofs to the removal of Says_Crypt_lost and Says_Crypt_not_lost
1997-06-18, by paulson
Deleted spurious reference to Spy_not_see_NB, which by chance was defined
1997-06-18, by paulson
converse -> ^-1
1997-06-17, by nipkow
Type constraint added to ensure that "length" refers to lists. Maybe should
1997-06-16, by paulson
Replacing the primrec definition of "length" by a translation to the built-in
1997-06-16, by paulson
Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas.
1997-06-13, by nipkow
changed compatible definition;
1997-06-13, by mueller
added deadlock
1997-06-12, by mueller
added deadlock freedom, polished definitions and proofs
1997-06-12, by mueller
Strengthened and streamlined the Yahalom proofs
1997-06-09, by paulson
Useful new lemma
1997-06-09, by paulson
eliminated non-ASCII;
1997-06-06, by wenzelm
Added
1997-06-06, by nipkow
improved function 'nonreserved'
1997-06-06, by oheimb
Removed a few redundant additions of simprules or classical rules
1997-06-06, by paulson
The name bex_conj_distrib was WRONG
1997-06-06, by paulson
Better miniscoping for bounded quantifiers
1997-06-06, by paulson
Tidying and simplification of declarations
1997-06-06, by paulson
Much polishing of proofs
1997-06-06, by paulson
New miniscoping rules for ALL
1997-06-06, by paulson
New facts about In0/1 by Burkhart Wolff
1997-06-06, by paulson
New miniscoping rules ball_triv and bex_triv
1997-06-06, by paulson
Mended the definition of ack(0,n)
1997-06-06, by paulson
Two new examples; corrected a comment
1997-06-06, by paulson
New example theory: Recdef
1997-06-06, by paulson
added finite_converse
1997-06-05, by nipkow
Moved image_is_empty from Finite.ML to equalities.ML
1997-06-05, by nipkow
Modified a few defs and proofs because of the changes to theory Finite.thy.
1997-06-05, by nipkow
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
1997-06-05, by nipkow
New recdef examples
1997-06-05, by paulson
Removal of freeze_vars and thaw_vars. New freeze_thaw
1997-06-05, by paulson
freezeT now refers to Type.freeze_thaw
1997-06-05, by paulson
Tidying of signature. More robust renaming in freeze_thaw.
1997-06-05, by paulson
Removal of freeze_vars and thaw_vars (quite unused...)
1997-06-05, by paulson
Removal of radixstring from string_of_int; addition of string_of_indexname
1997-06-05, by paulson
There was never need for another copy of radixstring...
1997-06-05, by paulson
Numerous simplifications and removal of HOL-isms
1997-06-05, by paulson
Now loads theory Recdef
1997-06-05, by paulson
A slight simplification of optstring
1997-06-05, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
1997-06-05, by paulson
Deleted the obsolete "pred_list" relation
1997-06-05, by paulson
Documented the new distinct_subgoals_tac
1997-06-05, by paulson
A slight simplification of optstring
1997-06-05, by paulson
Now extracts the predicate variable from induct0 insteead of trying to
1997-06-05, by paulson
Made the pseudo-type of split_rule_var a separate argument
1997-06-05, by paulson
eliminated non-ASCII;
1997-06-04, by wenzelm
eliminated freeze_vars;
1997-06-04, by wenzelm
changed priority of -> from [6,5]5 to [1,0]0
1997-06-04, by mueller
is_blank: fixed space2;
1997-06-03, by wenzelm
No longer refers to internal TFL structures
1997-06-03, by paulson
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
1997-06-03, by paulson
New theory "Power" of exponentiation (and binomial coefficients)
1997-06-03, by paulson
New theorem about the cardinality of the powerset (uses exponentiation)
1997-06-03, by paulson
Type inference makes a Const here, perhaps elsewhere?thry.sml
1997-06-02, by paulson
poly_tvars allows recdefs to be made without type constraints
1997-06-02, by paulson
Corrected banner: it is W0, not MiniML
1997-06-02, by paulson
New statement and proof of free_tv_subst_var in order to cope with new
1997-06-02, by paulson
Now Un_insert_left, Un_insert_right are default rewrite rules
1997-06-02, by paulson
Corrected statement of filter_append; added filter_size
1997-06-02, by paulson
Simplified proof
1997-06-02, by paulson
New theorems le_add_diff_inverse, le_add_diff_inverse2
1997-06-02, by paulson
trivial changes to incorporate CTL.thy and Example.ML in html file;
1997-05-30, by mueller
Simplified the calling sequence of CONTEXT_REWRITE_RULE
1997-05-30, by paulson
Moved "less_eq" to NatDef from Arith
1997-05-30, by paulson
New results including the basis for unique factorization
1997-05-30, by paulson
Now "primes" is a set
1997-05-30, by paulson
Now Divides must be the parent
1997-05-30, by paulson
New proofs about cardinality. Suggested by Florian Kammueller
1997-05-30, by paulson
less
more
|
(0)
-3000
-1000
-240
+240
+1000
+3000
+10000
+30000
tip