# HG changeset patch
# User wenzelm
# Date 950186078 -3600
# Node ID d67db92897df5196ad0cdefbcb255cddcddf6789
# Parent  07284f7ad26211d419c16d636c6f61eac3d91491
add_judgment;

diff -r 07284f7ad262 -r d67db92897df src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Thu Feb 10 11:08:42 2000 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Thu Feb 10 13:34:38 2000 +0100
@@ -4,8 +4,8 @@
 
 Automatic term bindings -- logic specific patterns.
 
-The implementation below works fine with the more common
-object-logics, such as HOL, ZF.
+Note: the current implementation is not quite 'generic', but works
+fine with the more common object-logics (HOL, FOL, ZF etc.).
 *)
 
 signature AUTO_BIND =
@@ -13,6 +13,8 @@
   val goal: term -> (indexname * term option) list
   val facts: string -> term list -> (indexname * term option) list
   val atomic_thesis: term -> (string * term) * term
+  val add_judgment: bstring * string * mixfix -> theory -> theory
+  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
 end;
 
 structure AutoBind: AUTO_BIND =
@@ -22,6 +24,8 @@
 val thisN = "this";
 
 
+(** bindings **)
+
 (* goal *)
 
 fun statement_binds (name, prop) =
@@ -55,6 +59,14 @@
 
 fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = ((thesisN, t), c $ mk_free t)
   | atomic_thesis t = ((thesisN, t), mk_free t);
-      
+
+
+(** judgment **)
+
+fun gen_add_judgment add args = PureThy.local_path o add [args] o PureThy.global_path;
+
+val add_judgment = gen_add_judgment Theory.add_consts;
+val add_judgment_i = gen_add_judgment Theory.add_consts_i;
+
 
 end;
diff -r 07284f7ad262 -r d67db92897df src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Feb 10 11:08:42 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 10 13:34:38 2000 +0100
@@ -125,6 +125,10 @@
 
 (* consts and syntax *)
 
+val judgmentP =
+  OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
+    (P.const -- P.marg_comment >> (Toplevel.theory o IsarThy.add_judgment));
+
 val constsP =
   OuterSyntax.command "consts" "declare constants" K.thy_decl
     (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts));
@@ -620,8 +624,8 @@
   text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
   (*theory sections*)
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
-  aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
-  constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP,
+  aritiesP, judgmentP, constsP, syntaxP, translationsP, axiomsP,
+  defsP, constdefsP, theoremsP, lemmasP, globalP, localP, useP, mlP,
   ml_commandP, ml_setupP, setupP, parse_ast_translationP,
   parse_translationP, print_translationP, typed_print_translationP,
   print_ast_translationP, token_translationP, oracleP,
diff -r 07284f7ad262 -r d67db92897df src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Feb 10 11:08:42 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Feb 10 13:34:38 2000 +0100
@@ -41,6 +41,8 @@
     -> theory -> theory
   val add_trrules: ((xstring * string) Syntax.trrule * Comment.text) list -> theory -> theory
   val add_trrules_i: (Syntax.ast Syntax.trrule * Comment.text) list -> theory -> theory
+  val add_judgment: (bstring * string * mixfix) * Comment.text -> theory -> theory
+  val add_judgment_i: (bstring * typ * mixfix) * Comment.text -> theory -> theory
   val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory
   val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list
     -> theory -> theory
@@ -207,7 +209,8 @@
 fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore;
 val add_trrules = Theory.add_trrules o map Comment.ignore;
 val add_trrules_i = Theory.add_trrules_i o map Comment.ignore;
-
+val add_judgment = AutoBind.add_judgment o Comment.ignore;
+val add_judgment_i = AutoBind.add_judgment_i o Comment.ignore;
 
 
 (* axioms and defs *)