isabelle: src/HOL/Argo.thy@7082c5df5df6 (annotated)

63960 3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	1	(* Title: HOL/Argo.thy
3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	2	Author: Sascha Boehme
3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	3	*)
3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	4
3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	5	theory Argo
3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	6	imports HOL
3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	7	begin
3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	8
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	9	ML_file \<open>~~/src/Tools/Argo/argo_expr.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	10	ML_file \<open>~~/src/Tools/Argo/argo_term.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	11	ML_file \<open>~~/src/Tools/Argo/argo_lit.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	12	ML_file \<open>~~/src/Tools/Argo/argo_proof.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	13	ML_file \<open>~~/src/Tools/Argo/argo_rewr.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	14	ML_file \<open>~~/src/Tools/Argo/argo_cls.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	15	ML_file \<open>~~/src/Tools/Argo/argo_common.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	16	ML_file \<open>~~/src/Tools/Argo/argo_cc.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	17	ML_file \<open>~~/src/Tools/Argo/argo_simplex.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	18	ML_file \<open>~~/src/Tools/Argo/argo_thy.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	19	ML_file \<open>~~/src/Tools/Argo/argo_heap.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	20	ML_file \<open>~~/src/Tools/Argo/argo_cdcl.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	21	ML_file \<open>~~/src/Tools/Argo/argo_core.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	22	ML_file \<open>~~/src/Tools/Argo/argo_clausify.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	23	ML_file \<open>~~/src/Tools/Argo/argo_solver.ML\<close>
63960 3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	24
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63960 diff changeset	25	ML_file \<open>Tools/Argo/argo_tactic.ML\<close>
63960 3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	26
3daf02070be5 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic boehmes parents: diff changeset	27	end

author	wenzelm
	Sat, 31 Dec 2022 14:58:34 +0100
changeset 76850	7082c5df5df6
parent 69605	a96320074298
permissions	-rw-r--r--