add_judgment;
authorwenzelm
Thu Feb 10 13:34:38 2000 +0100 (2000-02-10 ago)
changeset 8227d67db92897df
parent 8226 07284f7ad262
child 8228 8283e416b680
add_judgment;
src/Pure/Isar/auto_bind.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Thu Feb 10 11:08:42 2000 +0100
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Thu Feb 10 13:34:38 2000 +0100
     1.3 @@ -4,8 +4,8 @@
     1.4  
     1.5  Automatic term bindings -- logic specific patterns.
     1.6  
     1.7 -The implementation below works fine with the more common
     1.8 -object-logics, such as HOL, ZF.
     1.9 +Note: the current implementation is not quite 'generic', but works
    1.10 +fine with the more common object-logics (HOL, FOL, ZF etc.).
    1.11  *)
    1.12  
    1.13  signature AUTO_BIND =
    1.14 @@ -13,6 +13,8 @@
    1.15    val goal: term -> (indexname * term option) list
    1.16    val facts: string -> term list -> (indexname * term option) list
    1.17    val atomic_thesis: term -> (string * term) * term
    1.18 +  val add_judgment: bstring * string * mixfix -> theory -> theory
    1.19 +  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
    1.20  end;
    1.21  
    1.22  structure AutoBind: AUTO_BIND =
    1.23 @@ -22,6 +24,8 @@
    1.24  val thisN = "this";
    1.25  
    1.26  
    1.27 +(** bindings **)
    1.28 +
    1.29  (* goal *)
    1.30  
    1.31  fun statement_binds (name, prop) =
    1.32 @@ -55,6 +59,14 @@
    1.33  
    1.34  fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = ((thesisN, t), c $ mk_free t)
    1.35    | atomic_thesis t = ((thesisN, t), mk_free t);
    1.36 -      
    1.37 +
    1.38 +
    1.39 +(** judgment **)
    1.40 +
    1.41 +fun gen_add_judgment add args = PureThy.local_path o add [args] o PureThy.global_path;
    1.42 +
    1.43 +val add_judgment = gen_add_judgment Theory.add_consts;
    1.44 +val add_judgment_i = gen_add_judgment Theory.add_consts_i;
    1.45 +
    1.46  
    1.47  end;
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Feb 10 11:08:42 2000 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 10 13:34:38 2000 +0100
     2.3 @@ -125,6 +125,10 @@
     2.4  
     2.5  (* consts and syntax *)
     2.6  
     2.7 +val judgmentP =
     2.8 +  OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
     2.9 +    (P.const -- P.marg_comment >> (Toplevel.theory o IsarThy.add_judgment));
    2.10 +
    2.11  val constsP =
    2.12    OuterSyntax.command "consts" "declare constants" K.thy_decl
    2.13      (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
    2.14 @@ -620,8 +624,8 @@
    2.15    text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
    2.16    (*theory sections*)
    2.17    classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
    2.18 -  aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
    2.19 -  constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP,
    2.20 +  aritiesP, judgmentP, constsP, syntaxP, translationsP, axiomsP,
    2.21 +  defsP, constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP,
    2.22    ml_commandP, ml_setupP, setupP, parse_ast_translationP,
    2.23    parse_translationP, print_translationP, typed_print_translationP,
    2.24    print_ast_translationP, token_translationP, oracleP,
     3.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Feb 10 11:08:42 2000 +0100
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Feb 10 13:34:38 2000 +0100
     3.3 @@ -41,6 +41,8 @@
     3.4      -> theory -> theory
     3.5    val add_trrules: ((xstring * string) Syntax.trrule * Comment.text) list -> theory -> theory
     3.6    val add_trrules_i: (Syntax.ast Syntax.trrule * Comment.text) list -> theory -> theory
     3.7 +  val add_judgment: (bstring * string * mixfix) * Comment.text -> theory -> theory
     3.8 +  val add_judgment_i: (bstring * typ * mixfix) * Comment.text -> theory -> theory
     3.9    val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
    3.10    val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list
    3.11      -> theory -> theory
    3.12 @@ -207,7 +209,8 @@
    3.13  fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore;
    3.14  val add_trrules = Theory.add_trrules o map Comment.ignore;
    3.15  val add_trrules_i = Theory.add_trrules_i o map Comment.ignore;
    3.16 -
    3.17 +val add_judgment = AutoBind.add_judgment o Comment.ignore;
    3.18 +val add_judgment_i = AutoBind.add_judgment_i o Comment.ignore;
    3.19  
    3.20  
    3.21  (* axioms and defs *)