isabelle-dev  

Messages by Thread

• included jfreechart sources break scala_project Fabian Huch
• Time limiting apply and by commands Lawrence Paulson via isabelle-dev
• NEWS: Simplifier declarations Florian Haftmann
• instantiate_laws.py in AFP entry Registers Florian Haftmann
• [PATCH] VSCode fix: Dynamic_Ouput JSON serialization error `Bad JSON value: isabelle.vscode.LSP$$$Lambda` Andreas Kurz via isabelle-dev
  • Re: [PATCH] VSCode fix: Dynamic_Ouput JSON serialization error `Bad JSON value: isabelle.vscode.LSP$$$Lambda` Makarius
  • Re: [PATCH] VSCode fix: Dynamic_Ouput JSON serialization error `Bad JSON value: isabelle.vscode.LSP$$$Lambda` Andreas Kurz via isabelle-dev
  • Re: Problems with unsupported Isabelle/PIDE editors Makarius
  • Re: Problems with unsupported Isabelle/PIDE editors Andreas Kurz via isabelle-dev
  • Re: Problems with unsupported Isabelle/PIDE editors Makarius
• Auto-insert error in current development version Lawrence Paulson via isabelle-dev
  • Re: Auto-insert error in current development version Makarius
• NEWS: Isabelle/jEdit F1 versus S+F1 Makarius
• NEWS: Isabelle/jEdit menus Makarius
• NEWS: Isabelle/jEdit hyperlinks and navigation Makarius
  • Re: NEWS: Isabelle/jEdit hyperlinks and navigation Makarius
• A Missing Lemma Dual to nn_integral_FTC_atLeast 伊藤洋介
  • Re: A Missing Lemma Dual to nn_integral_FTC_atLeast Lawrence Paulson via isabelle-dev
  • Re: A Missing Lemma Dual to nn_integral_FTC_atLeast 伊藤洋介
  • Re: A Missing Lemma Dual to nn_integral_FTC_atLeast Lawrence Paulson via isabelle-dev
  • Re: A Missing Lemma Dual to nn_integral_FTC_atLeast 伊藤洋介
• build_task Lawrence Paulson via isabelle-dev
  • Re: build_task Fabian Huch
• Update to jdk-21.0.10 Makarius
• The future of macos vs. macos_arm Makarius
  • Re: The future of macos vs. macos_arm Lawrence Paulson via isabelle-dev
  • Re: The future of macos vs. macos_arm Makarius
  • Re: The future of macos vs. macos_arm Makarius
  • Re: The future of macos vs. macos_arm Lawrence Paulson via isabelle-dev
  • Re: The future of macos vs. macos_arm Makarius
  • Re: The future of macos vs. macos_arm Lawrence Paulson via isabelle-dev
• NEWS: Multiple hyperlinks in PIDE Makarius
  • Re: NEWS: Multiple hyperlinks in PIDE Makarius
  • Re: NEWS: Multiple hyperlinks in PIDE Makarius
• NEWS: Isabelle2025-2 supersedes Isabelle2025-1 Makarius
• Thy_Info.use_thy_legacy removed Makarius
• NEWS: Build progress and interrupts in Isabelle/Scala Makarius
• NEWS Florian Haftmann
• duplicate key value violates unique constraint "isabelle_build_sessions_pkey" Florian Haftmann
  • Re: duplicate key value violates unique constraint "isabelle_build_sessions_pkey" Makarius
  • Re: duplicate key value violates unique constraint "isabelle_build_sessions_pkey" Tobias Nipkow
  • Re: duplicate key value violates unique constraint "isabelle_build_sessions_pkey" Makarius
  • Re: duplicate key value violates unique constraint "isabelle_build_sessions_pkey" Fabian Huch
  • Re: duplicate key value violates unique constraint "isabelle_build_sessions_pkey" Fabian Huch
  • Re: duplicate key value violates unique constraint "isabelle_build_sessions_pkey" Makarius
  • Re: duplicate key value violates unique constraint "isabelle_build_sessions_pkey" Makarius
• Final notice: release snapshot of Isabelle2025-1 tomorrow Makarius
  • Re: Final notice: release snapshot of Isabelle2025-1 tomorrow Makarius
• build.proof.cit.tum.de – Key (name)=(Shadow_DOM) already exists Florian Haftmann
  • Re: build.proof.cit.tum.de – Key (name)=(Shadow_DOM) already exists Achim D. Brucker
  • Re: build.proof.cit.tum.de – Key (name)=(Shadow_DOM) already exists Fabian Huch
• A different mouse issue Lawrence Paulson via isabelle-dev
• Incorrect result from signed right-shift when using Code_Target_Numeral Daniel Matichuk via isabelle-dev
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Makarius
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Makarius
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Daniel Matichuk via isabelle-dev
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Makarius
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Makarius
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Daniel Matichuk via isabelle-dev
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Florian Haftmann
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Makarius
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Makarius
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Makarius
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Florian Haftmann
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Peter Lammich
  • Re: Incorrect result from signed right-shift when using Code_Target_Numeral Makarius
• afp-2025-1 fork now available Gerwin Klein via isabelle-dev
• Java/AWT/Swing problem with text input boxes vs. mouse selection Makarius
• NEWS: Isabelle/jEdit: more robust and reactive mouse handler, notably for macOS with Magic Mouse Makarius
  • Re: NEWS: Isabelle/jEdit: more robust and reactive mouse handler, notably for macOS with Magic Mouse Lawrence Paulson via isabelle-dev
  • Re: NEWS: Isabelle/jEdit: more robust and reactive mouse handler, notably for macOS with Magic Mouse Makarius
• Fork of isabelle-dev vs. isabelle-release Makarius
• Re: [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms Lawrence Paulson via isabelle-dev
  • Re: [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms Makarius
  • Re: [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms Lawrence Paulson via isabelle-dev
  • Re: [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms Manuel Eberl
  • Re: [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms Lawrence Paulson via isabelle-dev
  • Re: [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms Makarius
  • Re: [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms Makarius
  • Re: [isabelle] Simplifier fails when dealing with mix of Pure and HOL terms Florian Haftmann
• OOM Errors in 8GB JVM builds, -XX:SoftMaxHeapSize Fabian Huch
  • Re: OOM Errors in 8GB JVM builds, -XX:SoftMaxHeapSize Makarius
  • Re: OOM Errors in 8GB JVM builds, -XX:SoftMaxHeapSize Fabian Huch
• Towards Isabelle2025-1-RC3 and AFP release Makarius
  • Re: Towards Isabelle2025-1-RC3 and AFP release Gerwin Klein via isabelle-dev
  • Re: Towards Isabelle2025-1-RC3 and AFP release Makarius
  • Re: Towards Isabelle2025-1-RC3 and AFP release Makarius
  • Re: Towards Isabelle2025-1-RC3 and AFP release Makarius
  • Re: Towards Isabelle2025-1-RC3 and AFP release Tobias Nipkow
  • Re: Towards Isabelle2025-1-RC3 and AFP release Makarius
  • Towards Isabelle2025-1-RC3 and AFP release Makarius
• Servers offline Fabian Huch
  • Re: Servers offline Fabian Huch
• NEWS: Isabelle_System.ML_process vs. "isabelle ML_process" Makarius
• AFP entry Neural_Networks Lawrence Paulson via isabelle-dev
  • Re: AFP entry Neural_Networks Achim D. Brucker
  • Re: AFP entry Neural_Networks Lawrence Paulson via isabelle-dev
  • Re: [Afp-submit] AFP entry Neural_Networks Peter Lammich
  • Re: [Afp-submit] AFP entry Neural_Networks Achim D. Brucker
  • Re: [Afp-submit] AFP entry Neural_Networks Makarius
  • Re: [Afp-submit] AFP entry Neural_Networks Lawrence Paulson via isabelle-dev
  • Re: [Afp-submit] AFP entry Neural_Networks Peter Lammich
• Towards Isabelle2025-1-RC2 Makarius
  • Re: Towards Isabelle2025-1-RC2 Makarius
• NEWS: updates on Isabelle/VSCode Makarius
• More attacks by dump AI-bots Makarius
  • Re: More attacks by dump AI-bots Makarius
  • Re: More attacks by dump AI-bots Achim D. Brucker
  • Re: More attacks by dump AI-bots Makarius
  • Re: More attacks by dump AI-bots Achim D. Brucker
  • Re: More attacks by dump AI-bots Makarius
  • Re: More attacks by dump AI-bots Makarius
  • Re: More attacks by dump AI-bots Makarius
• zombie proof processes Lawrence Paulson via isabelle-dev
  • Re: zombie proof processes Manuel Eberl
  • Re: zombie proof processes Makarius
  • Re: zombie proof processes Peter Lammich
  • Re: zombie proof processes Makarius
  • Re: zombie proof processes Peter Lammich
  • Re: zombie proof processes Peter Lammich
  • Re: zombie proof processes Lawrence Paulson via isabelle-dev
  • Re: zombie proof processes Peter Lammich
  • Re: zombie proof processes Makarius
  • Re: zombie proof processes Peter Lammich
  • Re: zombie proof processes Manuel Eberl
  • Re: zombie proof processes: veriT Makarius
  • Re: zombie proof processes: veriT Alexander Pach via isabelle-dev
  • Re: zombie proof processes: veriT Makarius
  • Re: zombie proof processes: veriT Makarius
  • Re: zombie proof processes: veriT Peter Lammich
  • Re: zombie proof processes Makarius
  • Re: zombie proof processes Makarius
  • Re: zombie proof processes Lawrence Paulson via isabelle-dev
  • Re: zombie proof processes Makarius
  • Re: zombie proof processes Lawrence Paulson via isabelle-dev
  • Re: zombie proof processes Makarius
• Testing macOS 26 Tahoe Makarius
  • Re: Testing macOS 26 Tahoe Lawrence Paulson via isabelle-dev
  • Re: Testing macOS 26 Tahoe Makarius
• NEWS: support for screen reader technology in Isabelle/jEdit Makarius
• NEWS: Isabelle/VSCode GUI panels Makarius
• Problem in AFP Florian Haftmann
  • Problem in AFP Florian Haftmann
  • Re: Problem in AFP Makarius
• Towards Isabelle2025-1-RC1 Makarius
  • Re: Towards Isabelle2025-1-RC1 Makarius
  • Re: Towards Isabelle2025-1-RC1 Makarius
• Problem in AFP / AutoCorres2_Main Florian Haftmann
  • Re: Problem in AFP / AutoCorres2_Main Lawrence Paulson via isabelle-dev
• NEWS: Discontinue isabelle process -T / use_thy Makarius
• NEWS: update to polyml-5.9.2 Makarius
• Architecture problem Lawrence Paulson via isabelle-dev
  • Re: Architecture problem Makarius
  • Re: Architecture problem Makarius
  • Re: Architecture problem Lawrence Paulson via isabelle-dev
  • Re: Architecture problem Makarius
  • Re: Architecture problem Lawrence Paulson via isabelle-dev
  • Re: Architecture problem Makarius
  • Re: Architecture problem Jasmin Blanchette
  • Re: Architecture problem Makarius
  • Re: Architecture problem Lawrence Paulson via isabelle-dev
  • Re: Architecture problem Tobias Nipkow
  • Re: Architecture problem Jasmin Blanchette
  • Re: Architecture problem Manuel Eberl
  • Re: Architecture problem Lawrence Paulson via isabelle-dev
  • Re: Architecture problem Jasmin Blanchette
  • Re: Architecture problem Mathias Fleury
  • Re: Architecture problem Tjark Weber
  • Re: Architecture problem Jasmin Blanchette
  • Re: Architecture problem Lawrence Paulson via isabelle-dev
  • Re: Architecture problem Lawrence Paulson via isabelle-dev
  • Re: Architecture problem Lawrence Paulson via isabelle-dev
• NEWS: More detailed build progress Makarius
• Isabelle2025-1-RC0 available for experimentation Makarius
  • Re: Isabelle2025-1-RC0 available for experimentation Makarius
• build cluster: java.lang.OutOfMemoryError: Java heap space Makarius
• Significant slowdown of HOL-ex and HOL-Codegenerator_Test Makarius
  • Re: Significant slowdown of HOL-ex and HOL-Codegenerator_Test Lawrence Paulson via isabelle-dev
• Isabelle/VSCode: update to recent VSCodium 1.104 Makarius
• Plan for Isabelle2025-1 (December 2025) Makarius
• »invalid request« for isabelle build_task Florian Haftmann
  • Re: »invalid request« for isabelle build_task Fabian Huch
  • Re: »invalid request« for isabelle build_task Florian Haftmann
• Actuarial_Mathematics FAILED Florian Haftmann
• Update to jdk-21.0.8 Makarius
• Off-line? Lawrence Paulson via isabelle-dev
  • Re: Off-line? Fabian Huch
• Noteble slowdown of AFP/Native_Word Makarius
  • Re: Noteble slowdown of AFP/Native_Word Florian Haftmann
  • Re: Noteble slowdown of AFP/Native_Word Makarius
  • Re: Noteble slowdown of AFP/Native_Word Florian Haftmann
• Slowdown of AFP/SC_DOM_Components due to changes in "code-only operations" Makarius
  • Re: Slowdown of AFP/SC_DOM_Components due to changes in "code-only operations" Florian Haftmann
• NEWS: More uniform and scalable declarations of intro/elim/dest rules Makarius
  • Re: NEWS: More uniform and scalable declarations of intro/elim/dest rules Florian Haftmann
  • Re: NEWS: More uniform and scalable declarations of intro/elim/dest rules Makarius
• Default case for non-exhaustive primrec definitions? Elliot Bobrow
  • Re: Default case for non-exhaustive primrec definitions? Dmitriy Traytel via isabelle-dev
• SMT reconstruction failures Fabian Huch
  • Re: SMT reconstruction failures Jasmin Blanchette

• Earlier messages