diff options
Diffstat (limited to '')
| -rw-r--r-- | spartan/core/Spartan.thy (renamed from spartan/theories/Spartan.thy) | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/spartan/theories/Spartan.thy b/spartan/core/Spartan.thy index d235041..b4f7772 100644 --- a/spartan/theories/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -142,20 +142,20 @@ section \<open>Proof commands\<close> named_theorems typechk -ML_file \<open>../lib/lib.ML\<close> -ML_file \<open>../lib/goals.ML\<close> -ML_file \<open>../lib/focus.ML\<close> +ML_file \<open>lib.ML\<close> +ML_file \<open>goals.ML\<close> +ML_file \<open>focus.ML\<close> section \<open>Congruence automation\<close> (*Potential to be retired*) -ML_file \<open>../lib/congruence.ML\<close> +ML_file \<open>congruence.ML\<close> section \<open>Methods\<close> -ML_file \<open>../lib/elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close> +ML_file \<open>elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close> named_theorems intros and comps lemmas @@ -165,7 +165,7 @@ lemmas [comps] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong -ML_file \<open>../lib/tactics.ML\<close> +ML_file \<open>tactics.ML\<close> method_setup assumptions = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD ( @@ -227,7 +227,7 @@ ML_file "~~/src/Tools/misc_legacy.ML" ML_file "~~/src/Tools/IsaPlanner/isand.ML" ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" ML_file "~~/src/Tools/IsaPlanner/zipper.ML" -ML_file "../lib/eqsubst.ML" +ML_file "eqsubst.ML" \<comment> \<open>\<open>rewrite\<close> method\<close> consts rewrite_HOLE :: "'a::{}" ("\<hole>") @@ -254,7 +254,7 @@ lemma imp_cong_eq: done ML_file \<open>~~/src/HOL/Library/cconv.ML\<close> -ML_file \<open>../lib/rewrite.ML\<close> +ML_file \<open>rewrite.ML\<close> \<comment> \<open>\<open>reduce\<close> computes terms via judgmental equalities\<close> setup \<open>map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "" typechk_tac))\<close> @@ -273,7 +273,7 @@ consts iarg :: \<open>'a\<close> ("?") hole :: \<open>'b\<close> ("{}") -ML_file \<open>../lib/implicits.ML\<close> +ML_file \<open>implicits.ML\<close> attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close> |