isabelle: src/HOL/Try0.thy@da14e77a48b2 (annotated)

82343 56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	1	(* Title: HOL/Try0.thy
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	2	Author: Jasmin Blanchette, LMU Muenchen
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	3	Author: Martin Desharnais, LMU Muenchen
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	4	Author: Fabian Huch, TU Muenchen
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	5	*)
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	6
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	7	theory Try0
82360 6a09257afd06 moved try0's HOL-specific stuff into own theory desharna parents: 82359 diff changeset	8	imports Pure
82343 56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	9	keywords "try0" :: diag
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	10	begin
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	11
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	12	ML_file \<open>Tools/try0.ML\<close>
82363 3a7fc54b50ca tuned and moved configuration of auto_try0 to theory HOL desharna parents: 82360 diff changeset	13	ML_file \<open>Tools/try0_util.ML\<close>
3a7fc54b50ca tuned and moved configuration of auto_try0 to theory HOL desharna parents: 82360 diff changeset	14
3a7fc54b50ca tuned and moved configuration of auto_try0 to theory HOL desharna parents: 82360 diff changeset	15	ML \<open>
3a7fc54b50ca tuned and moved configuration of auto_try0 to theory HOL desharna parents: 82360 diff changeset	16	val () =
3a7fc54b50ca tuned and moved configuration of auto_try0 to theory HOL desharna parents: 82360 diff changeset	17	Try0.register_proof_method "simp" {run_if_auto_try = true}
3a7fc54b50ca tuned and moved configuration of auto_try0 to theory HOL desharna parents: 82360 diff changeset	18	(Try0_Util.apply_raw_named_method "simp" false Try0_Util.simp_attrs Simplifier_Trace.disable)
3a7fc54b50ca tuned and moved configuration of auto_try0 to theory HOL desharna parents: 82360 diff changeset	19	handle Symtab.DUP _ => ()
3a7fc54b50ca tuned and moved configuration of auto_try0 to theory HOL desharna parents: 82360 diff changeset	20	\<close>
82343 56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	21
56098b36c49f moved command try0 into its own new theory desharna parents: diff changeset	22	end

author	Manuel Eberl <manuel@pruvisto.org>
	Tue, 15 Apr 2025 17:38:20 +0200
changeset 82518	da14e77a48b2
parent 82363	3a7fc54b50ca
permissions	-rw-r--r--