Tree [7ee079] default tip / thys /
 History

Read Only access


File Date Author Commit
 AVL-Trees 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 AWN 2014-03-15 kleing kleing [06e363] added mathpartir
 Abortable_Linearizable_Modules 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Abstract-Hoare-Logics 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Abstract-Rewriting 2013-10-17 René Thiemann René Thiemann [96cce0] simplified proofs
 Abstract_Completeness 2014-04-16 paulson paulson [4b2efa] Abstract_Completeness files
 ArrowImpossibilityGS 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 AutoFocus-Stream 2013-07-29 kleing kleing [85728b] merged from release
 Automatic_Refinement 2014-05-29 nipkow nipkow [639f0b] greek not needed and breaks some tex installations
 BDD 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 BinarySearchTree 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Binomial-Heaps 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Binomial-Queues 2013-07-29 kleing kleing [85728b] merged from release
 Bondy 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Boolean_Expression_Checkers 2014-06-08 nipkow nipkow [36d784] New entry: Boolean Expression Checkers
 Bounded_Deducibility_Security unknown
 BytecodeLogicJmlTypes 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 CAVA_Automata 2014-05-29 nipkow nipkow [1e0232] New entry CAVA_Automata
 CAVA_LTL_Modelchecker 2014-05-30 nipkow nipkow [b28fe2] completed bibliography
 CCS 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 CISC-Kernel 2014-07-18 kleing kleing [b7f7f6] new entry: CISC-Kernel
 Category 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Category2 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Cauchy 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Circus 2013-08-23 wenzelm wenzelm [72bcd3] eliminated MS-DOS control characters;
 ClockSynchInst 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 CofGroups 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Coinductive 2013-10-18 Andreas Lochbihler Andreas Lochbihler [b6576c] add lemma
 Coinductive_Languages 2013-12-04 kleing kleing [848abf] include entry in AFP group
 Collections 2013-10-24 lammich lammich [c32d75] Added map_pick_remove - operation
 Compiling-Exceptions-Correctly 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Completeness 2013-07-29 kleing kleing [85728b] merged from release
 ComponentDependencies unknown
 Containers 2013-10-23 lammich lammich [796dc2] Moved instantiations for unit-type to common th...
 CoreC++ 2013-08-13 kuncar kuncar [581621] adapt to Isabelle/cb82606b8215
 CryptoBasedCompositionalProperties 2014-01-13 kleing kleing [1e2504] normalised ROOT file
 DPT-SAT-Solver 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 DataRefinementIBP 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Datatype_Order_Generator 2013-10-18 lammich lammich [9f85a3] Adapted Refine_Monadic, Collections, and depend...
 Decreasing-Diagrams 2013-12-02 kleing kleing [bd4a4f] avoid mentioning $AFP in entries, so things als...
 Depth-First-Search 2013-07-29 kleing kleing [85728b] merged from release
 Dijkstra_Shortest_Path 2013-10-18 lammich lammich [9f85a3] Adapted Refine_Monadic, Collections, and depend...
 Discrete_Summation 2014-04-13 nipkow nipkow [3ddac3] new entry Discrete_Summation
 DiskPaxos 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Efficient-Mergesort 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Example-Submission 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 FFT 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 FOL-Fitting 2013-07-29 kleing kleing [85728b] merged from release
 FeatherweightJava 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Featherweight_OCL 2014-01-16 paulson paulson [f548d1] Featherweight_OCL website, also fixes
 Fermat3_4 2013-07-29 kleing kleing [85728b] merged from release
 FileRefinement 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 FinFun 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Finger-Trees 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Flyspeck-Tame 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 FocusStreamsCaseStudies 2013-11-18 paulson paulson [50bc80] website for new entry FocusStreamsCaseStudies
 Free-Boolean-Algebra 2013-07-29 kleing kleing [85728b] merged from release
 Free-Groups 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 FunWithFunctions 2013-07-29 kleing kleing [85728b] merged from release
 FunWithTilings 2013-07-29 kleing kleing [85728b] merged from release
 Functional-Automata 2013-07-29 kleing kleing [85728b] merged from release
 GPU_Kernel_PL 2014-04-05 kleing kleing [06b8cd] GPU kernel PL entry by John Wickerson
 Gabow_SCC 2014-05-29 nipkow nipkow [febd77] New entry CAVA_LTL_Modelchecker
 Gauss-Jordan-Elim-Fun 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 GenClock 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 General-Triangle 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Girth_Chromatic 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 GoedelGod 2013-11-18 paulson paulson [1eb468] new entry GoedelGod
 GraphMarkingIBP 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Graph_Theory 2013-11-17 gerwin.klein@nicta.com.au gerwin.klein@nicta.com.au [6e6e37] chapter AFP for Graph_Theory
 Group-Ring-Module 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 HRB-Slicing 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Heard_Of 2013-08-23 wenzelm wenzelm [72bcd3] eliminated MS-DOS control characters;
 HereditarilyFinite 2013-11-17 paulson paulson [c84e45] new entry HereditarilyFinite
 HotelKeyCards 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Huffman 2013-08-13 wenzelm wenzelm [f5d0ba] standardized symbols via "isabelle update_sub_s...
 HyperCTL 2014-04-20 kleing kleing [22a9fa] tweaked ROOT file
 IEEE_Floating_Point 2014-04-16 paulson paulson [f53d83] Configuration file missing all this time??
 Impossible_Geometry 2013-08-23 wenzelm wenzelm [b8ce58] prefer line-oriented sources;
 Incompleteness 2013-12-02 kleing kleing [bd4a4f] avoid mentioning $AFP in entries, so things als...
 Inductive_Confidentiality 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 InformationFlowSlicing 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Integration 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Jinja 2013-08-13 wenzelm wenzelm [f5d0ba] standardized symbols via "isabelle update_sub_s...
 JinjaThreads 2013-10-21 Andreas Lochbihler Andreas Lochbihler [291284] adapt JinjaThreads to changes in Coinductive an...
 JiveDataStoreModel 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 KAT_and_DRA 2014-01-30 kleing kleing [9409c1] use relative paths
 KBPs 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 Kleene_Algebra 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 Koenigsberg_Friendship 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 LTL_to_GBA 2014-05-29 nipkow nipkow [4006a4] New entry LTL_to_GBA
 Lam-ml-Normalization 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 LatticeProperties 2013-08-23 wenzelm wenzelm [72bcd3] eliminated MS-DOS control characters;
 Launchbury 2014-05-25 kleing kleing [edcac8] build document graph
 Lazy-Lists-II 2013-10-18 Andreas Lochbihler Andreas Lochbihler [0367a3] use coinduction method and get rid of boilerpla...
 Lehmer 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 LightweightJava 2013-07-29 kleing kleing [85728b] merged from release
 LinearQuantifierElim 2013-09-23 blanchet blanchet [473bb5] merge
 List-Index 2013-09-23 blanchet blanchet [473bb5] merge
 List-Infinite 2013-07-29 kleing kleing [85728b] merged from release
 Locally-Nameless-Sigma 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Lower_Semicontinuous 2013-09-17 Brian Huffman Brian Huffman [611613] renamed lemma mem_convex_2 to convexD (cf. Isab...
 MSO_Regex_Equivalence 2014-06-12 nipkow nipkow [fff0d5] new entry MSO_Regex_Equivalence
 Markov_Models 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 Marriage 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Matrix 2013-10-18 Rene Thiemann Rene Thiemann [d7c732] added map_upto_split lemma
 Max-Card-Matching 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 MiniML 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 MonoBoolTranAlgebra 2013-08-23 wenzelm wenzelm [72bcd3] eliminated MS-DOS control characters;
 MuchAdoAboutTwo 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Myhill-Nerode 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Nat-Interval-Logic 2013-08-26 wenzelm wenzelm [6d69e4] removed junk;
 Native_Word 2013-09-24 kleing kleing [3a02c9] add entry to AFP group
 Network_Security_Policy_Verification 2014-07-09 nipkow nipkow [4c0b21] New entry Network_Security_Policy_Verification
 Nominal2 2013-09-28 Christian Urban Christian Urban [e6f981] synchronised Nominal2 and its AFP version (most...
 Noninterference_CSP 2014-05-25 kleing kleing [1f0f6b] new entry Noninterference_CSP
 NormByEval 2013-08-23 wenzelm wenzelm [7d0467] prefer plain subscript for notation;
 Open_Induction 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Ordinal 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Ordinals_and_Cardinals 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Ordinary_Differential_Equations 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 PCF 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 POPLmark-deBruijn 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 Partial_Function_MR 2014-02-19 nipkow nipkow [2a4644] new entry Partial_Function_MR
 Perfect-Number-Thm 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Pi_Calculus 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 Polynomials 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Pop_Refinement 2014-07-03 paulson paulson [e8d9a5] new entry Pop_Refinement
 Possibilistic_Noninterference 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Pratt_Certificate 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Presburger-Automata 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Probabilistic_Noninterference 2014-04-06 kleing kleing [59358d] avoid $AFP reference for regression test
 Program-Conflict-Analysis 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Promela 2014-05-29 nipkow nipkow [e44b35] New entry Promela
 PseudoHoops 2013-08-23 wenzelm wenzelm [72bcd3] eliminated MS-DOS control characters;
 Psi_Calculi 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 RIPEMD-160-SPARK 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 RSAPSS 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Ramsey-Infinite 2013-07-29 kleing kleing [85728b] merged from release
 Random_Graph_Subgraph_Threshold 2014-02-14 nipkow nipkow [e1d2f8] New entry Random_Graph_Subgraph_Threshold
 Rank_Nullity_Theorem 2013-08-23 wenzelm wenzelm [72bcd3] eliminated MS-DOS control characters;
 Real_Impl 2014-02-10 kleing kleing [56b2fd] entry by Rene Thiemann
 Recursion-Theory-I 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Refine_Monadic 2013-10-23 lammich lammich [796dc2] Moved instantiations for unit-type to common th...
 Regex_Equivalence 2014-01-30 nipkow nipkow [40b1ad] tuned
 Regular-Sets 2013-10-27 gerwin.klein@nicta.com.au gerwin.klein@nicta.com.au [5a0c76] import devel patch: separate theory for normali...
 Regular_Algebras 2014-05-22 nipkow nipkow [e5445f] new entry Regular_Algebras
 Relation_Algebra 2014-01-25 paulson paulson [588036] New entry Relation_Algebra
 Ribbon_Proofs 2013-10-02 kuncar kuncar [7ac434] use /HOL/Library/FSet and Lifting/Transfer
 Robbins-Conjecture 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Roy_Floyd_Warshall 2014-05-25 kleing kleing [bc2e84] new entry Roy_Floyd_Warshall
 SATSolverVerification 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 SIFPL 2013-07-29 kleing kleing [85728b] merged from release
 SIFUM_Type_Systems 2014-08-27 kleing kleing [7ee079] email address change Silvia Grewe
 Secondary_Sylow 2014-01-29 paulson paulson [75e0d0] new entry Secondary_Sylow
 Selection_Heap_Sort 2014-02-17 kleing kleing [096221] build on HOL-Library directly
 SenSocialChoice 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Separation_Algebra 2013-08-23 wenzelm wenzelm [5127ca] more standard method setup;
 Separation_Logic_Imperative_HOL 2013-10-18 lammich lammich [9f85a3] Adapted Refine_Monadic, Collections, and depend...
 SequentInvertibility 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Shivers-CFA 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 ShortestPath 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Simpl 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 Slicing 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Sort_Encodings 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Sqrt_Babylonian 2013-10-16 Rene Thiemann Rene Thiemann [1f8ee0] added algorithms to compute floor and ceiling o...
 Statecharts 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Stream-Fusion 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Strong_Security 2014-08-27 kleing kleing [7ee079] email address change Silvia Grewe
 Sturm_Sequences 2014-07-03 paulson paulson [e8d9a5] new entry Pop_Refinement
 Stuttering_Equivalence 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 SumSquares 2013-07-29 kleing kleing [85728b] merged from release
 TLA 2013-08-23 wenzelm wenzelm [9bf03e] more standard attribute setup;
 Tail_Recursive_Functions 2014-05-25 kleing kleing [8fbb75] contact details change requested by author
 Tarskis_Geometry 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Topology 2013-08-23 wenzelm wenzelm [9d8a3e] eliminated obsolete greek babel (see Isabelle/2...
 Transitive-Closure 2013-10-23 Rene Thiemann Rene Thiemann [54a733] no unfolding, which would lead to problems in c...
 Transitive-Closure-II 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Tree-Automata 2013-10-18 lammich lammich [9f85a3] Adapted Refine_Monadic, Collections, and depend...
 Tycon 2013-07-30 wenzelm wenzelm [3cf46e] type theory is purely value-oriented;
 Valuation 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 Verified-Prover 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 VolpanoSmith 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 WHATandWHERE_Security 2014-08-27 kleing kleing [7ee079] email address change Silvia Grewe
 Well_Quasi_Orders 2013-09-05 Christian Sternagel Christian Sternagel [e2b1da] recovered lost lemma (now a trivial corollary)
 WorkerWrapper 2013-08-23 wenzelm wenzelm [ec06b0] removed old machine-generated comments;
 pGCL 2014-07-13 kleing kleing [eaa1f4] new entry pGCL by David Cock
 LICENSE 2004-07-23 lsf37 lsf37 [376577] auto sync with Isabelle2004
 LICENSE.LGPL 2004-05-25 lsf37 lsf37 [b8330f] auto sync with Isabelle2004
 ROOTS 2014-07-18 kleing kleing [b7f7f6] new entry: CISC-Kernel

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

JavaScript is required for this form.





No, thanks