diff options
Diffstat (limited to 'spartan')
| -rw-r--r-- | spartan/core/Spartan.thy | 28 | ||||
| -rw-r--r-- | spartan/core/lib/congruence.ML (renamed from spartan/core/congruence.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/elimination.ML (renamed from spartan/core/elimination.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/eqsubst.ML (renamed from spartan/core/eqsubst.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/equality.ML (renamed from spartan/core/equality.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/focus.ML (renamed from spartan/core/focus.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/goals.ML (renamed from spartan/core/goals.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/implicits.ML (renamed from spartan/core/implicits.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/lib.ML (renamed from spartan/core/lib.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/rewrite.ML (renamed from spartan/core/rewrite.ML) | 0 | ||||
| -rw-r--r-- | spartan/core/lib/tactics.ML (renamed from spartan/core/tactics.ML) | 0 |
11 files changed, 14 insertions, 14 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 1d93885..4e53a45 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -112,7 +112,7 @@ syntax "_Sum" :: \<open>idt \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<clo translations "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sig A (\<lambda>x. B)" -abbreviation Prod (infixl "\<times>" 50) +abbreviation Prod (infixl "\<times>" 60) where "A \<times> B \<equiv> \<Sum>_: A. B" axiomatization where @@ -148,21 +148,21 @@ section \<open>Proof commands\<close> named_theorems typechk -ML_file \<open>lib.ML\<close> -ML_file \<open>goals.ML\<close> -ML_file \<open>focus.ML\<close> +ML_file \<open>lib/lib.ML\<close> +ML_file \<open>lib/goals.ML\<close> +ML_file \<open>lib/focus.ML\<close> section \<open>Congruence automation\<close> consts "rhs" :: \<open>'a\<close> ("..") -ML_file \<open>congruence.ML\<close> +ML_file \<open>lib/congruence.ML\<close> section \<open>Methods\<close> -ML_file \<open>elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close> +ML_file \<open>lib/elimination.ML\<close> \<comment> \<open>declares the [elims] attribute\<close> named_theorems intros and comps lemmas @@ -172,7 +172,7 @@ lemmas [comps] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong -ML_file \<open>tactics.ML\<close> +ML_file \<open>lib/tactics.ML\<close> method_setup assumptions = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD ( @@ -226,11 +226,11 @@ method_setup this = subsection \<open>Rewriting\<close> \<comment> \<open>\<open>subst\<close> method\<close> -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 "eqsubst.ML" +ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> +ML_file \<open>~~/src/Tools/IsaPlanner/isand.ML\<close> +ML_file \<open>~~/src/Tools/IsaPlanner/rw_inst.ML\<close> +ML_file \<open>~~/src/Tools/IsaPlanner/zipper.ML\<close> +ML_file \<open>lib/eqsubst.ML\<close> \<comment> \<open>\<open>rewrite\<close> method\<close> consts rewrite_HOLE :: "'a::{}" ("\<hole>") @@ -257,7 +257,7 @@ lemma imp_cong_eq: done ML_file \<open>~~/src/HOL/Library/cconv.ML\<close> -ML_file \<open>rewrite.ML\<close> +ML_file \<open>lib/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> @@ -276,7 +276,7 @@ consts iarg :: \<open>'a\<close> ("?") hole :: \<open>'b\<close> ("{}") -ML_file \<open>implicits.ML\<close> +ML_file \<open>lib/implicits.ML\<close> attribute_setup implicit = \<open>Scan.succeed Implicits.implicit_defs_attr\<close> diff --git a/spartan/core/congruence.ML b/spartan/core/lib/congruence.ML index d9f4ffa..d9f4ffa 100644 --- a/spartan/core/congruence.ML +++ b/spartan/core/lib/congruence.ML diff --git a/spartan/core/elimination.ML b/spartan/core/lib/elimination.ML index 617f83e..617f83e 100644 --- a/spartan/core/elimination.ML +++ b/spartan/core/lib/elimination.ML diff --git a/spartan/core/eqsubst.ML b/spartan/core/lib/eqsubst.ML index ea6f098..ea6f098 100644 --- a/spartan/core/eqsubst.ML +++ b/spartan/core/lib/eqsubst.ML diff --git a/spartan/core/equality.ML b/spartan/core/lib/equality.ML index 023147b..023147b 100644 --- a/spartan/core/equality.ML +++ b/spartan/core/lib/equality.ML diff --git a/spartan/core/focus.ML b/spartan/core/lib/focus.ML index 1d8de78..1d8de78 100644 --- a/spartan/core/focus.ML +++ b/spartan/core/lib/focus.ML diff --git a/spartan/core/goals.ML b/spartan/core/lib/goals.ML index 9f394f0..9f394f0 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/lib/goals.ML diff --git a/spartan/core/implicits.ML b/spartan/core/lib/implicits.ML index 4d73c8d..4d73c8d 100644 --- a/spartan/core/implicits.ML +++ b/spartan/core/lib/implicits.ML diff --git a/spartan/core/lib.ML b/spartan/core/lib/lib.ML index 615f601..615f601 100644 --- a/spartan/core/lib.ML +++ b/spartan/core/lib/lib.ML diff --git a/spartan/core/rewrite.ML b/spartan/core/lib/rewrite.ML index f9c5d8e..f9c5d8e 100644 --- a/spartan/core/rewrite.ML +++ b/spartan/core/lib/rewrite.ML diff --git a/spartan/core/tactics.ML b/spartan/core/lib/tactics.ML index 0e7db43..0e7db43 100644 --- a/spartan/core/tactics.ML +++ b/spartan/core/lib/tactics.ML |