diff options
Diffstat (limited to 'mltt/core/MLTT.thy')
| -rw-r--r-- | mltt/core/MLTT.thy | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/mltt/core/MLTT.thy b/mltt/core/MLTT.thy index 96cbe96..ec923e2 100644 --- a/mltt/core/MLTT.thy +++ b/mltt/core/MLTT.thy @@ -25,11 +25,11 @@ let val typ = Simple_Syntax.read_typ fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range) in - Sign.del_syntax (Print_Mode.ASCII, true) + Sign.syntax false (Print_Mode.ASCII, true) [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3))] - #> Sign.del_syntax Syntax.mode_default + #> Sign.syntax false Syntax.mode_default [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3))] - #> Sign.add_syntax Syntax.mode_default + #> Sign.syntax true Syntax.mode_default [("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3fn _./ _)", [0, 3], 3))] end \<close> @@ -309,10 +309,16 @@ subsection \<open>Trivial proofs (modulo automatic discharge of side conditions) method_setup this = \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts => CHEADGOAL (SIDE_CONDS 0 - (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) + (CONTEXT_TACTIC' (fn ctxt => simp_tac (ctxt addsimps facts))) facts))))\<close> +method_setup infer = + \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts => + CHEADGOAL (SIDE_CONDS 0 + (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) + facts))))\<close> + subsection \<open>Rewriting\<close> consts compute_hole :: "'a::{}" ("\<hole>") @@ -564,5 +570,4 @@ Lemma (def) distribute_Sig: by typechk+ qed - end |