Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned types;
authorwenzelm
Mon, 20 Oct 1997 15:20:20 +0200
changeset 3956 d59fe4579004
parent 3955 9666a1ecf3a1
child 3957 7914990748ad
tuned types;
src/Pure/axclass.ML file | annotate | diff | comparison | revisions
src/Pure/sign.ML file | annotate | diff | comparison | revisions
src/Pure/theory.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/axclass.ML	Mon Oct 20 15:18:09 1997 +0200
+++ b/src/Pure/axclass.ML	Mon Oct 20 15:20:20 1997 +0200
@@ -10,9 +10,9 @@
   val add_thms_as_axms: (string * thm) list -> theory -> theory
   val add_classrel_thms: thm list -> theory -> theory
   val add_arity_thms: thm list -> theory -> theory
-  val add_axclass: rclass * xclass list -> (string * string) list
+  val add_axclass: bclass * xclass list -> (string * string) list
     -> theory -> theory
-  val add_axclass_i: rclass * class list -> (string * term) list
+  val add_axclass_i: bclass * class list -> (string * term) list
     -> theory -> theory
   val add_inst_subclass: xclass * xclass -> string list -> thm list
     -> tactic option -> theory -> theory
--- a/src/Pure/sign.ML	Mon Oct 20 15:18:09 1997 +0200
+++ b/src/Pure/sign.ML	Mon Oct 20 15:20:20 1997 +0200
@@ -5,10 +5,10 @@
 The abstract type "sg" of signatures.
 *)
 
-(*raw base names*)
-type rstring = string;
-type rclass = class;
-(*external pruned forms*)
+(*base names*)
+type bstring = string;
+type bclass = class;
+(*external forms -- partially qualified names*)
 type xstring = string;
 type xclass = class;
 type xsort = sort;
@@ -40,8 +40,8 @@
   val classK: string
   val typeK: string
   val constK: string
-  val full_name: sg -> rstring -> string
-  val base_name: string -> rstring
+  val full_name: sg -> bstring -> string
+  val base_name: string -> bstring
   val intern: sg -> string -> xstring -> string
   val extern: sg -> string -> string -> xstring
   val cond_extern: sg -> string -> string -> xstring
@@ -72,30 +72,30 @@
   val infer_types: sg -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> xterm list * typ -> int * term * (indexname * typ) list
-  val add_classes: (rclass * xclass list) list -> sg -> sg
-  val add_classes_i: (rclass * class list) list -> sg -> sg
+  val add_classes: (bclass * xclass list) list -> sg -> sg
+  val add_classes_i: (bclass * class list) list -> sg -> sg
   val add_classrel: (xclass * xclass) list -> sg -> sg
   val add_classrel_i: (class * class) list -> sg -> sg
   val add_defsort: xsort -> sg -> sg
   val add_defsort_i: sort -> sg -> sg
-  val add_types: (rstring * int * mixfix) list -> sg -> sg
-  val add_tyabbrs: (rstring * string list * string * mixfix) list -> sg -> sg
-  val add_tyabbrs_i: (rstring * string list * typ * mixfix) list -> sg -> sg
+  val add_types: (bstring * int * mixfix) list -> sg -> sg
+  val add_tyabbrs: (bstring * string list * string * mixfix) list -> sg -> sg
+  val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> sg -> sg
   val add_arities: (xstring * xsort list * xsort) list -> sg -> sg
   val add_arities_i: (string * sort list * sort) list -> sg -> sg
-  val add_consts: (rstring * string * mixfix) list -> sg -> sg
-  val add_consts_i: (rstring * typ * mixfix) list -> sg -> sg
-  val add_syntax: (rstring * string * mixfix) list -> sg -> sg
-  val add_syntax_i: (rstring * typ * mixfix) list -> sg -> sg
-  val add_modesyntax: (string * bool) * (rstring * string * mixfix) list -> sg -> sg
-  val add_modesyntax_i: (string * bool) * (rstring * typ * mixfix) list -> sg -> sg
+  val add_consts: (bstring * string * mixfix) list -> sg -> sg
+  val add_consts_i: (bstring * typ * mixfix) list -> sg -> sg
+  val add_syntax: (bstring * string * mixfix) list -> sg -> sg
+  val add_syntax_i: (bstring * typ * mixfix) list -> sg -> sg
+  val add_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
+  val add_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
   val add_trfuns:
-    (string * (ast list -> ast)) list *
-    (string * (term list -> term)) list *
-    (string * (term list -> term)) list *
-    (string * (ast list -> ast)) list -> sg -> sg
+    (bstring * (ast list -> ast)) list *
+    (bstring * (term list -> term)) list *
+    (bstring * (term list -> term)) list *
+    (bstring * (ast list -> ast)) list -> sg -> sg
   val add_trfunsT:
-    (string * (typ -> term list -> term)) list -> sg -> sg
+    (bstring * (typ -> term list -> term)) list -> sg -> sg
   val add_tokentrfuns:
     (string * string * (string -> string * int)) list -> sg -> sg
   val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
--- a/src/Pure/theory.ML	Mon Oct 20 15:18:09 1997 +0200
+++ b/src/Pure/theory.ML	Mon Oct 20 15:20:20 1997 +0200
@@ -37,41 +37,41 @@
   val thmK		: string
   val oracleK		: string
   (*theory extendsion primitives*)
-  val add_classes	: (rclass * xclass list) list -> theory -> theory
-  val add_classes_i	: (rclass * class list) list -> theory -> theory
+  val add_classes	: (bclass * xclass list) list -> theory -> theory
+  val add_classes_i	: (bclass * class list) list -> theory -> theory
   val add_classrel	: (xclass * xclass) list -> theory -> theory
   val add_classrel_i	: (class * class) list -> theory -> theory
   val add_defsort	: xsort -> theory -> theory
   val add_defsort_i	: sort -> theory -> theory
-  val add_types		: (rstring * int * mixfix) list -> theory -> theory
-  val add_tyabbrs	: (rstring * string list * string * mixfix) list
+  val add_types		: (bstring * int * mixfix) list -> theory -> theory
+  val add_tyabbrs	: (bstring * string list * string * mixfix) list
     -> theory -> theory
-  val add_tyabbrs_i	: (rstring * string list * typ * mixfix) list
+  val add_tyabbrs_i	: (bstring * string list * typ * mixfix) list
     -> theory -> theory
   val add_arities	: (xstring * xsort list * xsort) list -> theory -> theory
   val add_arities_i	: (string * sort list * sort) list -> theory -> theory
-  val add_consts	: (rstring * string * mixfix) list -> theory -> theory
-  val add_consts_i	: (rstring * typ * mixfix) list -> theory -> theory
-  val add_syntax	: (rstring * string * mixfix) list -> theory -> theory
-  val add_syntax_i	: (rstring * typ * mixfix) list -> theory -> theory
-  val add_modesyntax	: string * bool -> (rstring * string * mixfix) list -> theory -> theory
-  val add_modesyntax_i	: string * bool -> (rstring * typ * mixfix) list -> theory -> theory
+  val add_consts	: (bstring * string * mixfix) list -> theory -> theory
+  val add_consts_i	: (bstring * typ * mixfix) list -> theory -> theory
+  val add_syntax	: (bstring * string * mixfix) list -> theory -> theory
+  val add_syntax_i	: (bstring * typ * mixfix) list -> theory -> theory
+  val add_modesyntax	: string * bool -> (bstring * string * mixfix) list -> theory -> theory
+  val add_modesyntax_i	: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
   val add_trfuns	:
-    (string * (Syntax.ast list -> Syntax.ast)) list *
-    (string * (term list -> term)) list *
-    (string * (term list -> term)) list *
-    (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
+    (bstring * (Syntax.ast list -> Syntax.ast)) list *
+    (bstring * (term list -> term)) list *
+    (bstring * (term list -> term)) list *
+    (bstring * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
   val add_trfunsT	:
-    (string * (typ -> term list -> term)) list -> theory -> theory
+    (bstring * (typ -> term list -> term)) list -> theory -> theory
   val add_tokentrfuns:
     (string * string * (string -> string * int)) list -> theory -> theory
   val add_trrules	: (string * string) Syntax.trrule list -> theory -> theory
   val add_trrules_i	: Syntax.ast Syntax.trrule list -> theory -> theory
-  val add_axioms	: (rstring * string) list -> theory -> theory
-  val add_axioms_i	: (rstring * term) list -> theory -> theory
-  val add_oracle	: rstring * (Sign.sg * exn -> term) -> theory -> theory
-  val add_defs		: (rstring * string) list -> theory -> theory
-  val add_defs_i	: (rstring * term) list -> theory -> theory
+  val add_axioms	: (bstring * string) list -> theory -> theory
+  val add_axioms_i	: (bstring * term) list -> theory -> theory
+  val add_oracle	: bstring * (Sign.sg * exn -> term) -> theory -> theory
+  val add_defs		: (bstring * string) list -> theory -> theory
+  val add_defs_i	: (bstring * term) list -> theory -> theory
   val add_path		: string -> theory -> theory
   val add_space		: string * string list -> theory -> theory
   val add_name		: string -> theory -> theory
isabelle