stub for Isar command interface
authorhaftmann
Wed, 17 Nov 2010 11:26:39 +0100
changeset 40583 6fed6f946471
parent 40582 968c481aa18c
child 40584 28cc2acbc58a
stub for Isar command interface
src/HOL/Tools/functorial_mappers.ML
--- a/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 11:09:18 2010 +0100
+++ b/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 11:26:39 2010 +0100
@@ -147,4 +147,21 @@
         concatenate = concatenate, identity = identity }))
   end;
 
+fun gen_type_mapper prep_term raw_t thy =
+  let
+    val t = prep_term thy raw_t;
+    val after_qed = K I;
+  in
+    thy
+    |> Named_Target.theory_init
+    |> Proof.theorem NONE after_qed []
+  end
+
+val type_mapper = gen_type_mapper Sign.cert_term;
+val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
+
+val _ =
+  Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
+    (Parse.term >> (fn t => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd t))));
+
 end;