- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Mar 1 2021
Mar 1 2021
paulson <lp15@cam.ac.uk> committed rAFPde7a40fb511d: tidied up messy proofs.
tidied up messy proofs
makarius committed rISABELLEd045cdbdf243: proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);.
proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
dissolve theory with duplicated name from afp
florian.haftmann committed rAFPa41a4c9f031d: more connections between mset _ = mset _ and permutations.
more connections between mset _ = mset _ and permutations
lemma diffusion
florian.haftmann committed rISABELLEfd32f08f4fb5: more connections between mset _ = mset _ and permutations.
more connections between mset _ = mset _ and permutations
dissolve theory with duplicated name from afp
Feb 28 2021
Feb 28 2021
makarius committed rISABELLEa89f56ab2686: more robust (amending 87403fde8cc3): notably allow symlink to existing….
more robust (amending 87403fde8cc3): notably allow symlink to existing…
Feb 27 2021
Feb 27 2021
more Isabelle/ML/Scala operations;
more Isabelle/ML/Scala operations;
proper src1, amending 20157c8ab3f3;
more Isabelle/ML/Scala operations;
proper File.eq, amending df49ca5da9d0;
clarified modules: more like ML;
makarius committed rISABELLE8ae2f8ebc373: discontinued somewhat pointless "integrity test of build_history": it fails….
discontinued somewhat pointless "integrity test of build_history": it fails…
makarius committed rISABELLE87403fde8cc3: more direct make_directory in ML and Scala, but ssh still requires perl for….
more direct make_directory in ML and Scala, but ssh still requires perl for…
clarified comments;
clarified message;
Feb 26 2021
Feb 26 2021
nipkow committed rISABELLEc8e317a4c905: improved list_neq simproc.
improved list_neq simproc
revert accidental change
fix typo (Bauer -> Bayer)
add Windows example to use-instructions
paulson <lp15@cam.ac.uk> committed rAFPcb1f24a06749: Formal_Puiseux_Series website.
Formal_Puiseux_Series website
Isabelle app layout changed on Mac
paulson <lp15@cam.ac.uk> committed rAFP74a42283f683: new entry Formal_Puiseux_Series.
new entry Formal_Puiseux_Series
update with 2021 release .tar.gz's
add Isabelle2021 release date
update .tar.gz releases
Feb 25 2021
Feb 25 2021
repaired document
Feb 24 2021
Feb 24 2021
paulson <lp15@cam.ac.uk> committed rISABELLE915b3d41dec1: A couple of basic lemmas about arg.
A couple of basic lemmas about arg
emphasize connection to multisets
multiset as equivalence class of permuted lists
multiset as equivalence class of permuted lists
emphasize connection to multisets
makarius committed rISABELLE43ce3b8a25ee: proper "latest" tag, otherwise the default pull command from https://hub.docker..
proper "latest" tag, otherwise the default pull command from https://hub.docker.
Feb 23 2021
Feb 23 2021
Susannah Mansky <susannahej@gmail.com> committed rAFP3b6c0a05c5cf: Updating Jinja from apply-style to Isar-style.
Updating Jinja from apply-style to Isar-style
more on Isabelle_System.bash;
more specific name
more specific name
dropped obscure FIXME
desharna committed rISABELLEf0210642e43f: proper usage of hypotheses for zipperposition's TPTP generation.
proper usage of hypotheses for zipperposition's TPTP generation
desharna committed rISABELLEf84a93f1de2f: tuned Mirabelle to parse option check_trivial only once.
tuned Mirabelle to parse option check_trivial only once
desharna committed rISABELLEa34b49841585: added stride option to Mirabelle.
added stride option to Mirabelle
desharna committed rISABELLEf6f1242ed367: proper prover capabilities for zipperposition.
proper prover capabilities for zipperposition
Feb 22 2021
Feb 22 2021
adapted to Isabelle/0110e2e2964c;
adapted to Isabelle/f0db1e4c89bc;
more direct timing from bash_process wrapper;
makarius committed rISABELLE0e7a3c055f39: clarified uses of Isabelle_System.bash_process: more checks, fewer messages;.
clarified uses of Isabelle_System.bash_process: more checks, fewer messages;
clarified signature, following Isabelle/Scala;
makarius committed rISABELLE7dbae202ff84: clarified signature: Isabelle_System.bash_process is strict and thus cannot….
clarified signature: Isabelle_System.bash_process is strict and thus cannot…
clarified signature;
makarius committed rISABELLE0110e2e2964c: clarified signature: always trim_line of Process_Result.out/err, uniformly in….
clarified signature: always trim_line of Process_Result.out/err, uniformly in…
clarified signature, following Isabelle/Scala;
makarius committed rISABELLE17c28251fff0: clarified signature: process_result timing from Isabelle/Scala;.
clarified signature: process_result timing from Isabelle/Scala;
get rid of traditional predicate
florian.haftmann committed rISABELLE05a873f90655: dedicated locale for preorder and abstract bdd operation.
dedicated locale for preorder and abstract bdd operation
get rid of traditional predicate
florian.haftmann committed rAFPf8f24482ab45: dedicated locale for preorder and abstract bdd operation.
dedicated locale for preorder and abstract bdd operation
dcjm committed rPOLYMLe1c3b8b57002: Reset the C stack pointer after a call to a C function on Unix 64-bits. This… (authored by dcjm).
Reset the C stack pointer after a call to a C function on Unix 64-bits. This…
dcjm committed rPOLYML795465d5c91e: Change type of touchClosure to 'a closure -> unit. Allow "load" in the… (authored by dcjm).
Change type of touchClosure to 'a closure -> unit. Allow "load" in the…
dcjm committed rPOLYML2c090e1e8175: Print the exception if an ML callback raises an exception. (authored by dcjm).
Print the exception if an ML callback raises an exception.
dcjm committed rPOLYMLa07c58e9a829: Fix shift constants. They did not take account of the tag shift. (authored by dcjm).
Fix shift constants. They did not take account of the tag shift.
Feb 21 2021
Feb 21 2021
more accurate process_result;
makarius committed rISABELLEc8abfe393c16: more accurate process_result in ML, corresponding to Process_Result in Scala;.
more accurate process_result in ML, corresponding to Process_Result in Scala;
proper treatment of process_result;
clarified: proper trim_line for error;