| Author | Object | Transaction | Date |
|---|
| makarius | rISABELLEc6c4069a86f3: tuned signature; | | Mar 30 2023, 4:10 PM |
| makarius | rISABELLE8db468bd1ec6: more operations for profiling; | | Mar 30 2023, 4:09 PM |
| makarius | rISABELLE44a6ac96314d: provide rsync component, with uniform version + options on all platforms; | | Mar 30 2023, 4:04 PM |
| makarius | rISABELLE2abc452d0ee9: tuned message; | | Mar 30 2023, 4:02 PM |
| makarius | rISABELLEf73400337c5c: provide local component to remote directory; | | Mar 30 2023, 3:33 PM |
| makarius | rISABELLE04a250facd44: tuned output; | | Mar 30 2023, 3:31 PM |
| makarius | rISABELLE34178d26a360: more SSH operations; | | Mar 30 2023, 2:25 PM |
| makarius | rISABELLEf513f754c026: more operations; | | Mar 30 2023, 12:56 PM |
| makarius | rISABELLE2e3c7c557151: tuned comments; | | Mar 30 2023, 12:10 PM |
| makarius | rISABELLE49d38fa1478d: clarified directory names, following bash_process (see e59d7d6fe1bd); | | Mar 30 2023, 12:03 PM |
| makarius | rISABELLEefd5c582d7ae: tuned README; | | Mar 30 2023, 11:58 AM |
| makarius | rISABELLE12c8d72df48a: clarified build options; | | Mar 30 2023, 11:40 AM |
| Christian Urban <christian.urban@kcl.ac.uk> | rAFPf0dfd9de026b: added more simplification rules involving Zero | | Mar 30 2023, 10:32 AM |
| makarius | rISABELLEfea7bc828b8b: more portable options; | | Mar 29 2023, 10:40 PM |
| makarius | rISABELLE2b5b093a1c08: build rsync from sources, to avoid divergence of protocols on various platforms; | | Mar 29 2023, 10:21 PM |
| makarius | rISABELLE1951f6470792: discontinue somewhat pointless is_single, which also depends on details of… | | Mar 29 2023, 10:02 PM |
| makarius | rISABELLE33bee7a96f72: tuned comments (amending 1951f6470792); | | Mar 29 2023, 10:02 PM |
| makarius | rISABELLE1208ece65cca: more informative errors; | | Mar 29 2023, 9:28 PM |
| makarius | rISABELLE7ac59361791e: clarified options; | | Mar 29 2023, 9:23 PM |
| makarius | rISABELLEa8c52c99fa92: tuned messages; | | Mar 29 2023, 9:16 PM |
| makarius | rISABELLE4649c7bfd3f0: provide Isabelle tool wrapper; | | Mar 29 2023, 8:56 PM |
| makarius | rISABELLE5a2a297a91f8: more robust errors: proceed updating database; | | Mar 29 2023, 8:41 PM |
| makarius | rISABELLEca46ff5b4fa1: tuned; | | Mar 29 2023, 3:02 PM |
| makarius | rISABELLE4855150bc98b: tuned output; | | Mar 29 2023, 2:59 PM |
| makarius | rISABELLEebf70b199db7: clarified signature; | | Mar 29 2023, 2:52 PM |
| makarius | rISABELLE1398add8c414: clarified modules; | | Mar 29 2023, 2:22 PM |
| makarius | rAFPb5968e0969d7: adapted to Isabelle/4a174bea55e2; | | Mar 29 2023, 12:37 PM |
| makarius | rISABELLE4a174bea55e2: prefer Sortset.T for shyps; | | Mar 29 2023, 12:37 PM |
| makarius | rAFPb5968e0969d7: adapted to Isabelle/4a174bea55e2; | | Mar 29 2023, 12:35 PM |
| makarius | rISABELLE33bee7a96f72: tuned comments (amending 1951f6470792); | | Mar 29 2023, 12:25 PM |
| makarius | rISABELLE676713cba24d: tuned; | | Mar 29 2023, 12:24 PM |
| makarius | rISABELLE1951f6470792: discontinue somewhat pointless is_single, which also depends on details of… | | Mar 29 2023, 12:05 PM |
| makarius | rISABELLE19c539f5d4d3: more compact data: approx. 0.85 .. 1.10 of plain list size; | | Mar 29 2023, 12:02 PM |
| makarius | rISABELLE2225d3267f58: slightly more compact data; | | Mar 29 2023, 10:34 AM |
| makarius | rISABELLEe64428b6b170: more operations, notably for profiling; | | Mar 28 2023, 11:16 PM |
| makarius | rISABELLE81d553e9428d: tuned; | | Mar 28 2023, 10:46 PM |
| makarius | rISABELLE570f1436fe0a: more compact representation of leaf nodes: only 1.10 .. 1.33 larger than plain… | | Mar 28 2023, 10:43 PM |
| makarius | rISABELLEbe3f838b3e17: tuned --- fewer compiler warnings; | | Mar 28 2023, 7:43 PM |
| makarius | rISABELLEc4c96a833a37: tuned; | | Mar 28 2023, 7:40 PM |
| makarius | rISABELLE59c94a376a3c: tuned; | | Mar 28 2023, 7:07 PM |
| makarius | rISABELLE7d014af40072: tuned; | | Mar 28 2023, 7:03 PM |
| makarius | rISABELLE48fbecc8fab1: tuned signature: more uniform structure Key; | | Mar 28 2023, 6:10 PM |
| makarius | rISABELLE4a174bea55e2: prefer Sortset.T for shyps; | | Mar 28 2023, 5:59 PM |
| makarius | rISABELLE0ad86d5b3bc3: tuned; | | Mar 28 2023, 5:51 PM |
| makarius | rISABELLEb0d3951232ad: more operations; | | Mar 28 2023, 5:32 PM |
| makarius | rISABELLEb98edf66ca96: tuned names: "e" means "entry" in table.ML and "elem" in set.ML; | | Mar 28 2023, 5:30 PM |
| makarius | rISABELLE6ae930c89143: NEWS; | | Mar 27 2023, 10:17 PM |
| makarius | rISABELLE96a594e5e054: added Set.size; | | Mar 27 2023, 10:11 PM |
| makarius | rISABELLEb4032c468d74: performanc tuning: avoid exception overhead, potentially relevant for Sorts. | | Mar 27 2023, 9:53 PM |
| makarius | rISABELLEb761c91c2447: performance tuning: prefer functor Set() over Table(); | | Mar 27 2023, 9:48 PM |
| makarius | rISABELLE8faf28a80a7f: efficient representation of sets: more compact than Table.set; | | Mar 27 2023, 7:41 PM |
| nipkow | rAFPb6c8736b79bb: New entry No_FTL_observers_Gen_Rel | | Mar 27 2023, 6:12 PM |
| makarius | rISABELLE7c1cc9ce9340: tuned whitespace; | | Mar 27 2023, 4:24 PM |
| makarius | rISABELLEf750047e9386: tuned comments; | | Mar 27 2023, 11:52 AM |
| makarius | rISABELLEcbfbf48b0281: tuned signature; | | Mar 26 2023, 8:03 PM |
| makarius | rISABELLE6ad3a412ed97: clarified signature; | | Mar 26 2023, 7:51 PM |
| makarius | rISABELLE6a2daddc238c: tuned signature; | | Mar 26 2023, 7:36 PM |
| makarius | rISABELLE3f4163b83d4f: tuned output; | | Mar 26 2023, 7:31 PM |
| makarius | rISABELLE236e43c8bb5b: support option tags; | | Mar 26 2023, 7:28 PM |
| makarius | rISABELLE27dd3a3fcc54: removed junk (amending 236e43c8bb5b); | | Mar 26 2023, 7:28 PM |
| nipkow | rAFP283b369461f2: uodated map update syntax | | Mar 26 2023, 5:42 PM |
| makarius | rISABELLE27dd3a3fcc54: removed junk (amending 236e43c8bb5b); | | Mar 26 2023, 3:47 PM |
| makarius | rISABELLEbe0b9396604e: tuned; | | Mar 26 2023, 3:02 PM |
| makarius | rISABELLE0d6e592d24c0: tuned output; | | Mar 26 2023, 2:45 PM |
| makarius | rISABELLEdd4bb80dbc3a: tuned performance: much faster low-level operation; | | Mar 26 2023, 2:36 PM |
| makarius | rISABELLE25fd62cba347: clarified signature: more general operation Bytes.read_slice; | | Mar 26 2023, 2:24 PM |
| makarius | rISABELLEb8b01343e3df: clarified signature: more explicit types; | | Mar 26 2023, 12:53 PM |
| makarius | rISABELLE53dc388b98ec: clarified signature: more explicit types; | | Mar 26 2023, 12:46 PM |
| makarius | rISABELLEf137bf5d3d94: clarified signature: more explicit types; | | Mar 26 2023, 12:41 PM |
| florian.haftmann | rAFP8b1d59d0990d: Adjusted to changes in distribution. | | Mar 24 2023, 7:30 PM |
| florian.haftmann | rISABELLEa6a81f848135: More explicit type information in dictionary arguments. | | Mar 24 2023, 7:30 PM |
| florian.haftmann | rISABELLEe6ee7af8184c: tuned whitespace | | Mar 24 2023, 7:30 PM |
| florian.haftmann | rISABELLE4c5297aa18c8: more uniform approach towards satisfied applications | | Mar 24 2023, 7:30 PM |
| florian.haftmann | rISABELLE0262155d2743: more uniform approach towards satisfied applications | | Mar 24 2023, 7:30 PM |
| florian.haftmann | rISABELLE5af3954ed6cf: tuned | | Mar 24 2023, 7:30 PM |
| florian.haftmann | rISABELLEb5fbe9837aee: tuned | | Mar 24 2023, 7:30 PM |
| florian.haftmann | rISABELLE86b9a405b0cc: Tuned semicolons. | | Mar 24 2023, 7:30 PM |
| florian.haftmann | rISABELLE596452389ad0: tuned | | Mar 24 2023, 7:30 PM |
| desharna | rISABELLEd5060a919b3f: reordered assumption and tuned proof of Multiset.bex_least_element and Multiset. | | Mar 20 2023, 6:33 PM |
| desharna | rISABELLE51ed312cabeb: added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element | | Mar 20 2023, 6:21 PM |
| desharna | rISABELLEf35cbb4da88a: refactored proofs | | Mar 20 2023, 3:02 PM |
| desharna | rISABELLE9c7cbad50e04: added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element | | Mar 20 2023, 3:01 PM |
| desharna | rISABELLE93531ba2c784: reversed import dependency between Relation and Finite_Set; and move theorems… | | Mar 20 2023, 3:01 PM |
| paulson | rISABELLE84a09beb682d: merged | | Mar 20 2023, 1:26 PM |
| makarius | rISABELLEea509b0bfc80: more operations; | | Mar 20 2023, 11:13 AM |
| makarius | rISABELLE068ff989c143: clarified theory_sizeof1_data: count bytes, individually for each data entry; | | Mar 20 2023, 11:09 AM |
| makarius | rISABELLE3e746e684f4b: clarified operations for ML object sizes; | | Mar 20 2023, 10:59 AM |
| paulson | rISABELLE125414e23e12: merged | | Mar 19 2023, 7:55 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE71d075d18b6e: simplified a lot of messy proofs | | Mar 19 2023, 7:55 PM |
| desharna | rISABELLE9b8770994780: merged | | Mar 18 2023, 11:48 PM |
| makarius | rISABELLE07e2cafcc97e: more operations; | | Mar 18 2023, 8:23 PM |
| paulson <lp15@cam.ac.uk> | rISABELLE48aa9928f090: Numerous significant simplifications | | Mar 17 2023, 6:06 PM |
| desharna | rISABELLE58b3913059fa: added lemma multp_repeat_mset_repeat_msetI | | Mar 17 2023, 1:56 PM |
| paulson | rISABELLE7969fa41439b: merged | | Mar 17 2023, 12:24 PM |
| makarius | rISABELLE3e8e749935fc: proper "build_thorough" for "isabelle update" (amending 9e5f8f6e58a0); | | Mar 17 2023, 12:11 PM |
| makarius | rISABELLE9e5f8f6e58a0: more thorough treatment of build prefs, guarded by system option… | | Mar 17 2023, 12:11 PM |
| makarius | rISABELLE3e8e749935fc: proper "build_thorough" for "isabelle update" (amending 9e5f8f6e58a0); | | Mar 17 2023, 12:10 PM |
| paulson | rISABELLE05329cd9db4b: merged | | Mar 17 2023, 11:42 AM |
| paulson <lp15@cam.ac.uk> | rISABELLE71f001027a13: Proof simplification | | Mar 17 2023, 11:42 AM |
| makarius | rAFPc3a4497b0f9d: more realistic timeout; | | Mar 17 2023, 11:02 AM |