Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

map marker$stmarker to Unwanted.id

  • Loading branch information...
commit 3e8ecc59fe4fc27c26cae97dbe1d5cb4d2fe2f1d 1 parent 29d37a6
@xrchz xrchz authored
Showing with 1 addition and 0 deletions.
  1. +1 −0  src/marker/markerScript.sml
View
1  src/marker/markerScript.sml
@@ -11,6 +11,7 @@ val _ = new_theory "marker";
---------------------------------------------------------------------- *)
val stmarker_def = new_definition("stmarker_def", ``stmarker (x:'a) = x``);
+val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy="marker",Name="stmarker"},name=(["Unwanted"],"id")}
(* the following move_<dir>_<op> theorems will loop if more than one term
is marked at the same level *)
Please sign in to comment.
Something went wrong with that request. Please try again.