diff options
| author | Josh Chen | 2020-07-31 18:10:10 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-31 18:10:10 +0200 |
| commit | 77aa10763429d2ded040071fbf7bee331dd52f5e (patch) | |
| tree | 266abca73311031798c3936c1e44827bda292f25 /spartan/lib/Prelude.thy | |
| parent | ff5454812f9e2720bd90c3a5437505644f63b487 (diff) | |
(REF) Tweak attribute names in preparation for new logical introduction rule behavior
Diffstat (limited to '')
| -rw-r--r-- | spartan/lib/Prelude.thy | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy index 36f12d2..6adbce8 100644 --- a/spartan/lib/Prelude.thy +++ b/spartan/lib/Prelude.thy @@ -43,8 +43,8 @@ axiomatization where lemmas [form] = SumF and - [intro] = Sum_inl Sum_inr and - [intros] = Sum_inl[rotated] Sum_inr[rotated] and + [intr] = Sum_inl Sum_inr and + [intro] = Sum_inl[rotated] Sum_inr[rotated] and [elim ?s] = SumE and [comp] = Sum_comp_inl Sum_comp_inr @@ -79,7 +79,7 @@ and lemmas [form] = TopF BotF and - [intro, intros] = TopI and + [intr, intro] = TopI and [elim ?a] = TopE and [elim ?x] = BotE and [comp] = Top_comp @@ -129,7 +129,7 @@ Lemma if_false: lemmas [form] = BoolF and - [intro, intros] = Bool_true Bool_false and + [intr, intro] = Bool_true Bool_false and [comp] = if_true if_false and [elim ?x] = ifelse lemmas |