diff options
| author | Josh Chen | 2020-08-05 15:21:43 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-08-05 15:21:43 +0200 |
| commit | c530305cbcafba9f66f1a55a1b5177a62f52535c (patch) | |
| tree | 2c4736cf5884e53edd0b8eaebb903bb3f4857d2f /spartan/core | |
| parent | 710f314a9ccb84cdd9df9bc8bf52482b8d1f5a56 (diff) | |
1. fix intros method. 2. Couple extra lemmas; good small test cases for normalization in typechecking/elaboration.
Diffstat (limited to 'spartan/core')
| -rw-r--r-- | spartan/core/Spartan.thy | 3 | ||||
| -rw-r--r-- | spartan/core/context_tactical.ML | 2 |
2 files changed, 3 insertions, 2 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index ea72208..7f13036 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -248,7 +248,8 @@ method_setup intros = K (CONTEXT_METHOD (fn facts => case n_opt of SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)) - | NONE => CREPEAT (CCHANGED (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))))))\<close> + | NONE => CCHANGED (CREPEAT (CCHANGED ( + CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)))))))\<close> method_setup elim = \<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD ( diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML index 0aa6f20..d0fed61 100644 --- a/spartan/core/context_tactical.ML +++ b/spartan/core/context_tactical.ML @@ -92,7 +92,7 @@ fun CREPEAT ctac = fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac -fun CREPEAT_N 0 _ = all_ctac +fun CREPEAT_N 0 _ = no_ctac | CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac fun CFILTER pred ctac cst = |