adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/lib/Eisbach_Tools
History
Gerwin Klein e76c69ee07 lib: provide warning suppression for Eisbach methods 
Contexts have the "visible" flag that determine whether warnings such
as duplicate rewrite rules are shown or not. Make setting this flag to
false available in Eisbach methods.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
 		2024-01-15 11:08:27 +11:00
..
Apply_Debug.thy lib/Eisbach_Tools: morphism type changed in Isabelle2023 2023-10-06 14:29:15 +11:00
Apply_Trace.thy lib/Eisbach_Tools: morphism type changed in Isabelle2023 2023-10-06 14:29:15 +11:00
Apply_Trace_Cmd.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
Conjuncts.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
Eisbach_Methods.thy lib: provide warning suppression for Eisbach methods 2024-01-15 11:08:27 +11:00
Local_Method.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
Local_Method_Tests.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
ProvePart.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
README.md lib: README.md files for the new sessions 2023-01-25 11:49:59 +11:00
ROOT lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
Rule_By_Method.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
Simp_No_Conditional.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
Subgoal_Methods.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
Trace_Schematic_Insts.thy lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00
tests.xml lib: add separate Eisbach_Tools session 2023-01-24 11:30:04 +11:00

README.md

Eisbach and Tactic Tools

This session contains tools and tactics for defining Isabelle Eisbach methods.

Some of the theories in this session are not strictly speaking Eisbach-related, but are mostly used from Eisbach methods, so we collect them here as well.

We only include theories that are needed in the Monads, CParser, and AutoCorres sessions.