Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged from afp-2016-1
  2. new entry: Minimal_SSA
  3. Bertrands_Postulate website
  4. Bertrand’s Postulate
  5. add new session to ROOTS
  6. new entry by Manuel Eberl
  7. New entry: UPF_Firewall
  8. Password_Authentication_Protocol
  9. new entry Password_Authentication_Protocol
  10. New article: FOL_Harrison
  11. New entry: Concurrent_Ref_Alg
  12. Twelvefold_Way website
  13. Twelvefold_Way
  14. New entry: Proof_Strategy_Language
Changeset 7586:81786077a578 by kleing:
merged from afp-2016-1
Changeset 7585:1d9a6dcae08a by nipkow:
new entry: Minimal_SSA
The file was addedthys/Minimal_SSA/Irreducible.thy
The file was addedthys/Minimal_SSA/ROOT
The file was addedthys/Minimal_SSA/document/root.bib
The file was addedthys/Minimal_SSA/document/root.tex
The file was addedweb/entries/Minimal_SSA.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/Formal_SSA.shtml (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7584:5e0ea96cf11c by paulson _lp15@cam.ac.uk_:
Bertrands_Postulate website
The file was addedweb/entries/Bertrands_Postulate.shtml
The file was modified metadata/metadata (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7583:bcbcf5535a3f by paulson _lp15@cam.ac.uk_:
Bertrand’s Postulate
The file was addedthys/Bertrands_Postulate/Bertrand.thy
The file was addedthys/Bertrands_Postulate/Bertrand_Discrete_Sqrt.thy
The file was addedthys/Bertrands_Postulate/ROOT
The file was addedthys/Bertrands_Postulate/bertrand.ML
The file was addedthys/Bertrands_Postulate/document/root.bib
The file was addedthys/Bertrands_Postulate/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 7582:ff54e4419f27 by gerwin klein _gerwin.klein@nicta.com.au_:
add new session to ROOTS
The file was modified thys/ROOTS (diff)
Changeset 7581:27fa96881f09 by gerwin klein _gerwin.klein@nicta.com.au_:
new entry by Manuel Eberl
The file was addedthys/E_Transcendental/E_Transcendental.thy
The file was addedthys/E_Transcendental/ROOT
The file was addedthys/E_Transcendental/document/root.bib
The file was addedthys/E_Transcendental/document/root.tex
The file was addedweb/entries/E_Transcendental.shtml
The file was modified metadata/metadata (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7580:aa27d34cd374 by nipkow:
New entry: UPF_Firewall
The file was addedthys/UPF_Firewall/Examples/DMZ/DMZ.thy
The file was addedthys/UPF_Firewall/Examples/DMZ/DMZDatatype.thy
The file was addedthys/UPF_Firewall/Examples/DMZ/DMZInteger.thy
The file was addedthys/UPF_Firewall/Examples/Examples.thy
The file was addedthys/UPF_Firewall/Examples/NAT-FW/NAT-FW.thy
The file was addedthys/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewall.thy
The file was addedthys/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallDatatype.thy
The file was addedthys/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallInt.thy
The file was addedthys/UPF_Firewall/Examples/PersonalFirewall/PersonalFirewallIpv4.thy
The file was addedthys/UPF_Firewall/Examples/Transformation/Transformation.thy
The file was addedthys/UPF_Firewall/Examples/Transformation/Transformation01.thy
The file was addedthys/UPF_Firewall/Examples/Transformation/Transformation02.thy
The file was addedthys/UPF_Firewall/Examples/VoIP/VoIP.thy
The file was addedthys/UPF_Firewall/FWNormalisation/ElementaryRules.thy
The file was addedthys/UPF_Firewall/FWNormalisation/FWNormalisation.thy
The file was addedthys/UPF_Firewall/FWNormalisation/FWNormalisationCore.thy
The file was addedthys/UPF_Firewall/FWNormalisation/NormalisationGenericProofs.thy
The file was addedthys/UPF_Firewall/FWNormalisation/NormalisationIPPProofs.thy
The file was addedthys/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy
The file was addedthys/UPF_Firewall/NAT/NAT.thy
The file was addedthys/UPF_Firewall/PacketFilter/DatatypeAddress.thy
The file was addedthys/UPF_Firewall/PacketFilter/DatatypePort.thy
The file was addedthys/UPF_Firewall/PacketFilter/IPv4.thy
The file was addedthys/UPF_Firewall/PacketFilter/IPv4_TCPUDP.thy
The file was addedthys/UPF_Firewall/PacketFilter/IntegerAddress.thy
The file was addedthys/UPF_Firewall/PacketFilter/IntegerPort.thy
The file was addedthys/UPF_Firewall/PacketFilter/IntegerPort_TCPUDP.thy
The file was addedthys/UPF_Firewall/PacketFilter/NetworkCore.thy
The file was addedthys/UPF_Firewall/PacketFilter/NetworkModels.thy
The file was addedthys/UPF_Firewall/PacketFilter/PacketFilter.thy
The file was addedthys/UPF_Firewall/PacketFilter/PolicyCombinators.thy
The file was addedthys/UPF_Firewall/PacketFilter/PolicyCore.thy
The file was addedthys/UPF_Firewall/PacketFilter/PortCombinators.thy
The file was addedthys/UPF_Firewall/PacketFilter/Ports.thy
The file was addedthys/UPF_Firewall/PacketFilter/ProtocolPortCombinators.thy
The file was addedthys/UPF_Firewall/ROOT
The file was addedthys/UPF_Firewall/StatefulFW/FTP.thy
The file was addedthys/UPF_Firewall/StatefulFW/FTPVOIP.thy
The file was addedthys/UPF_Firewall/StatefulFW/FTP_WithPolicy.thy
The file was addedthys/UPF_Firewall/StatefulFW/LTL_alike.thy
The file was addedthys/UPF_Firewall/StatefulFW/StatefulCore.thy
The file was addedthys/UPF_Firewall/StatefulFW/StatefulFW.thy
The file was addedthys/UPF_Firewall/StatefulFW/VOIP.thy
The file was addedthys/UPF_Firewall/UPF-Firewall.thy
The file was addedthys/UPF_Firewall/document/introduction.tex
The file was addedthys/UPF_Firewall/document/root.bib
The file was addedthys/UPF_Firewall/document/root.tex
The file was addedweb/entries/UPF_Firewall.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/UPF.shtml (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7579:0898b4cefd15 by paulson _lp15@cam.ac.uk_:
Password_Authentication_Protocol
The file was addedweb/entries/Password_Authentication_Protocol.shtml
The file was modified metadata/metadata (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7578:82e9e4cac632 by paulson _lp15@cam.ac.uk_:
new entry Password_Authentication_Protocol
The file was addedthys/Password_Authentication_Protocol/Propaedeutics.thy
The file was addedthys/Password_Authentication_Protocol/Protocol.thy
The file was addedthys/Password_Authentication_Protocol/ROOT
The file was addedthys/Password_Authentication_Protocol/document/root.bib
The file was addedthys/Password_Authentication_Protocol/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 7577:1d5c2472710b by nipkow:
New article: FOL_Harrison
The file was addedthys/FOL_Harrison/FOL_Harrison.thy
The file was addedthys/FOL_Harrison/ROOT
The file was addedthys/FOL_Harrison/document/root.tex
The file was addedweb/entries/FOL_Harrison.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7576:f13444e53683 by nipkow:
New entry: Concurrent_Ref_Alg
The file was addedthys/Concurrent_Ref_Alg/CRA.thy
The file was addedthys/Concurrent_Ref_Alg/Conjunction.thy
The file was addedthys/Concurrent_Ref_Alg/Conjunctive_Iteration.thy
The file was addedthys/Concurrent_Ref_Alg/Conjunctive_Sequential.thy
The file was addedthys/Concurrent_Ref_Alg/Galois_Connections.thy
The file was addedthys/Concurrent_Ref_Alg/Infimum_Nat.thy
The file was addedthys/Concurrent_Ref_Alg/Iteration.thy
The file was addedthys/Concurrent_Ref_Alg/Parallel.thy
The file was addedthys/Concurrent_Ref_Alg/ROOT
The file was addedthys/Concurrent_Ref_Alg/Refinement_Lattice.thy
The file was addedthys/Concurrent_Ref_Alg/Rely_Quotient.thy
The file was addedthys/Concurrent_Ref_Alg/Sequential.thy
The file was addedthys/Concurrent_Ref_Alg/document/root.bib
The file was addedthys/Concurrent_Ref_Alg/document/root.tex
The file was addedweb/entries/Concurrent_Ref_Alg.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7575:49d13fd3d96f by paulson _lp15@cam.ac.uk_:
Twelvefold_Way website
The file was addedweb/entries/Twelvefold_Way.shtml
The file was modified web/entries/Bell_Numbers_Spivey.shtml (diff)
The file was modified web/entries/Card_Multisets.shtml (diff)
The file was modified web/entries/Card_Number_Partitions.shtml (diff)
The file was modified web/entries/Card_Partitions.shtml (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 7574:993e83128e09 by paulson _lp15@cam.ac.uk_:
Twelvefold_Way
The file was addedthys/Twelvefold_Way/Card_Bijections.thy
The file was addedthys/Twelvefold_Way/Card_Bijections_Direct.thy
The file was addedthys/Twelvefold_Way/Equiv_Relations_on_Functions.thy
The file was addedthys/Twelvefold_Way/Preliminaries.thy
The file was addedthys/Twelvefold_Way/ROOT
The file was addedthys/Twelvefold_Way/Twelvefold_Way.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Core.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry1.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry10.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry11.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry12.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry2.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry3.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry4.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry5.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry6.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry7.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry8.thy
The file was addedthys/Twelvefold_Way/Twelvefold_Way_Entry9.thy
The file was addedthys/Twelvefold_Way/document/root.bib
The file was addedthys/Twelvefold_Way/document/root.tex
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
Changeset 7573:54b51c6bcdf7 by nipkow:
New entry: Proof_Strategy_Language
The file was addedthys/Proof_Strategy_Language/Constructor_Class.ML
The file was addedthys/Proof_Strategy_Language/Dynamic_Tactic_Generation.ML
The file was addedthys/Proof_Strategy_Language/Example.thy
The file was addedthys/Proof_Strategy_Language/Instantiation.ML
The file was addedthys/Proof_Strategy_Language/Isar_Interface.ML
The file was addedthys/Proof_Strategy_Language/License.txt
The file was addedthys/Proof_Strategy_Language/Monadic_Prover.ML
The file was addedthys/Proof_Strategy_Language/PSL.thy
The file was addedthys/Proof_Strategy_Language/PSL_Parser.ML
The file was addedthys/Proof_Strategy_Language/Parser_Combinator.ML
The file was addedthys/Proof_Strategy_Language/ROOT
The file was addedthys/Proof_Strategy_Language/Subtool.ML
The file was addedthys/Proof_Strategy_Language/Try_Hard.thy
The file was addedthys/Proof_Strategy_Language/Utils.ML
The file was addedthys/Proof_Strategy_Language/document/root.bib
The file was addedthys/Proof_Strategy_Language/document/root.tex
The file was addedweb/entries/Proof_Strategy_Language.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/statistics.shtml (diff)
The file was modified web/topics.shtml (diff)