From cb4139dc35527bd8c8f9b70753c3d1f552c5f19d Mon Sep 17 00:00:00 2001 From: stuebinm Date: Wed, 29 Jun 2022 01:14:51 +0200 Subject: make mltt work with isabelle 2021-1 notably, this modifies the proof method `this`: the previous version of it no longer works with cconv.ML (borrowed from HOL), so now it's just a call to the simplifier, which does work. Unfortunately the new `this` can otherwise do less than the old one (it does not instantiate schematic variables), so the old one is now available as `infer` instead. --- mltt/core/MLTT.thy | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'mltt/core/MLTT.thy') 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 \ 'a \ logic", mixfix ("(3%_./ _)", [0, 3], 3))] - #> Sign.del_syntax Syntax.mode_default + #> Sign.syntax false Syntax.mode_default [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3\_./ _)", [0, 3], 3))] - #> Sign.add_syntax Syntax.mode_default + #> Sign.syntax true Syntax.mode_default [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3fn _./ _)", [0, 3], 3))] end \ @@ -309,10 +309,16 @@ subsection \Trivial proofs (modulo automatic discharge of side conditions) method_setup this = \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))))\ +method_setup infer = + \Scan.succeed (K (CONTEXT_METHOD (fn facts => + CHEADGOAL (SIDE_CONDS 0 + (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) + facts))))\ + subsection \Rewriting\ consts compute_hole :: "'a::{}" ("\") @@ -564,5 +570,4 @@ Lemma (def) distribute_Sig: by typechk+ qed - end -- cgit v1.2.3