# HG changeset patch
# User wenzelm
# Date 1217935896 -7200
# Node ID 0b22524c05e202a805aef1e0626fc11751d687cc
# Parent  cd1df29db6206624df270b6f83ce3967e8eb2d71
removed axiom;
added fact, dynamic_fact, prop;

diff -r cd1df29db620 -r 0b22524c05e2 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Aug 05 13:31:35 2008 +0200
+++ b/src/Pure/General/markup.ML	Tue Aug 05 13:31:36 2008 +0200
@@ -37,7 +37,8 @@
   val tyconN: string val tycon: string -> T
   val fixedN: string val fixed: string -> T
   val constN: string val const: string -> T
-  val axiomN: string val axiom: string -> T
+  val factN: string val fact: string -> T
+  val dynamic_factN: string val dynamic_fact: string -> T
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
@@ -50,6 +51,7 @@
   val sortN: string val sort: T
   val typN: string val typ: T
   val termN: string val term: T
+  val propN: string val prop: T
   val keywordN: string val keyword: string -> T
   val commandN: string val command: string -> T
   val keyword_declN: string val keyword_decl: string -> T
@@ -150,7 +152,8 @@
 val (tyconN, tycon) = markup_string "tycon" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (constN, const) = markup_string "const" nameN;
-val (axiomN, axiom) = markup_string "axiom" nameN;
+val (factN, fact) = markup_string "fact" nameN;
+val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 
 
 (* inner syntax *)
@@ -168,6 +171,7 @@
 val (sortN, sort) = markup_elem "sort";
 val (typN, typ) = markup_elem "typ";
 val (termN, term) = markup_elem "term";
+val (propN, prop) = markup_elem "prop";
 
 
 (* outer syntax *)