Activity for lp15
-
lp15 committed [016604]
tidied a definition and proof
-
Merge
-
removed a terrible default simprule
-
webpage for Delta_System_Lemma
-
New (ZF!) entry Delta_System_Lemma
-
A bit of tidying
-
A few tweaks
-
tidying up
-
A little more tidying up
-
more on "summable"
-
tidying for the new geometric simprule
-
A bit of tidying up
-
new entry Relational_Method
-
Relational_Method website
-
Updated version by author
-
adjusting for the re-orientation of order_unique_lemma
-
updated the email addresses of Popescu <https://www.andreipopescu.uk> and Traytel <https://traytel.bitbucket.io>
-
new entry Shadow_SC_DOM
-
Verified_SAT_Based_AI_Planning website [NB corrected some \cite commands and deleted some excess files]
-
fixed latex and .bib errors
-
The first of Achim D. Brucker's three entries
-
Entry for AI_Planning_Languages_Semantics, including new topic "Computer science/Artificial intelligence" and URLs for the authors
-
entry SC_DOM_Components
-
SC_DOM_Components website
-
website for Shadow_SC_DOM
-
Verified_SAT_Based_AI_Planning files
-
new entry AI_Planning_Languages_Semantics
-
website for Core_SC_DOM
-
fixed a nonterminating proof (caused by Algebra change)
-
trival
-
fixes for mult_less_iff1, mult_le_cancel_iff1, mult_le_cancel_iff2
-
patched some brittle apply-chains
-
Simplified some definitions and proofs by eliminating the constant cconcat
-
nice new version without even/odd case splits
-
removal of a synonym
-
Omit the now redundant premise
-
tweaks
-
removal of some theorem aliases involving "card"
-
fixed proofs — not sure why they were failing
-
new entry Syntax_Independent_Logic
-
sitegen for Syntax_Independent_Logic
-
sitegen for Robinson_Arithmetic
-
new entry Goedel_Incompleteness
-
Goedel_HFSet_Semanticless sitegen
-
missed for some reason
-
new entry Robinson_Arithmetic
-
sitegen Goedel_Incompleteness
-
new entry Goedel_HFSet_Semantic
-
sitegen for Goedel_HFSet_Semantic
-
Fixed broken links (missing quote)
-
fix for the new, simpler power_diff_1_eq
-
a tiny bit of beautification
-
new entry Inductive_Inference
-
sitegen for Inductive_Inference
-
a repair and considerable reformatting
-
removal of library theorems that were already in Isabelle main
-
variable renaming
-
the last quantifier tweaks
-
quantifier fixes
-
more on order types
-
some lex fixes
-
new entry Saturation_Framework_Extensions
-
more lex fixes, some tricky
-
more lex fixes
-
fixes for new-style definition of lexicographic ordering
-
new entry Chandy_Lamport
-
fixing some lex problems
-
sitegen for Chandy_Lamport
-
reversing all the lex crap
-
sitegen for Saturation_Framework_Extensions (and also for five other entries)
-
stronger * with + cancellation lemmas
-
getting rid of inj_on_image_mem_iff_alt
-
new theorems, esp. on order types
-
Forcing website
-
new entry Forcing
-
Recursion-Addition
-
Lambert_W website
-
correction of typos in the abstract (Banach-Steinhaus)
-
Removed reference identifiers from the abstract of Banach_Steinhaus
-
new entry Lambert_W
-
Banach_Steinhaus entry and website
-
sitegen for Recursion-Addition, plus fixed some typos in the abstract
-
sitegen
-
Max/Sup issue
-
corrections for Sup{} = (0::nat)
-
removal of legacy binding
-
Attack_Trees website
-
fixed a frac_le proof
-
fixed a failing frac_le proof
-
new entry Relational-Incorrectness-Logic
-
Relational-Incorrectness-Logic website
-
Grant acknowledgement for ALEXANDRIA (ERC Project 742178)
-
more fixes for alias issues (which for Auto2 means giving up)
-
elimination of some aliases
-
elimination of some aliases, etc.
-
Some new and/or generalised theorems
-
ZFC_in_HOL: Now with Cantor normal form!
-
fixed some TeX problems
-
A new lemma
-
some new lemmas
1 >