propp: 'concl' patterns;
authorwenzelm
Thu Jul 08 18:36:09 1999 +0200 (1999-07-08)
changeset 6935a3f3f4128cab
parent 6934 04d051190a5f
child 6936 ca17f1b02cde
propp: 'concl' patterns;
src/HOL/Tools/typedef_package.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/skip_proof.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Jul 08 18:35:44 1999 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Jul 08 18:36:09 1999 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4      val goal = Thm.term_of (goal_nonempty cset);
     1.5    in
     1.6      thy
     1.7 -    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, [])), comment) int
     1.8 +    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int
     1.9    end;
    1.10  
    1.11  val typedef_proof = gen_typedef_proof read_term;
     2.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Jul 08 18:35:44 1999 +0200
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Thu Jul 08 18:36:09 1999 +0200
     2.3 @@ -49,6 +49,7 @@
     2.4    val const: token list -> (bstring * string * Syntax.mixfix) * token list
     2.5    val term: token list -> string * token list
     2.6    val prop: token list -> string * token list
     2.7 +  val propp: token list -> (string * (string list * string list)) * token list
     2.8    val attribs: token list -> Args.src list * token list
     2.9    val opt_attribs: token list -> Args.src list * token list
    2.10    val thm_name: string -> token list -> (bstring * Args.src list) * token list
    2.11 @@ -223,6 +224,15 @@
    2.12  val prop = group "proposition" trm;
    2.13  
    2.14  
    2.15 +(* prop patters *)
    2.16 +
    2.17 +val is_props = Scan.repeat1 ($$$ "is" |-- prop);
    2.18 +val concl_props = $$$ "concl" |-- !!! is_props;
    2.19 +val any_props = is_props -- Scan.optional concl_props [] || concl_props >> pair [];
    2.20 +
    2.21 +val propp = prop -- Scan.optional ($$$ "(" |-- !!! (any_props --| $$$ ")")) ([], []);
    2.22 +
    2.23 +
    2.24  (* arguments *)
    2.25  
    2.26  val keyword_symid = Scan.one (OuterLex.keyword_pred OuterLex.is_sid) >> OuterLex.val_of;
     3.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Jul 08 18:35:44 1999 +0200
     3.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Jul 08 18:36:09 1999 +0200
     3.3 @@ -38,8 +38,8 @@
     3.4      val thm = Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof);
     3.5    in Method.METHOD (fn _ => ALLGOALS (Tactic.rtac thm)) end;
     3.6  
     3.7 -val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth);
     3.8 -val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth);
     3.9 +val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth, None);
    3.10 +val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth, None);
    3.11  
    3.12  
    3.13  (* proof command *)
     4.1 --- a/src/Pure/axclass.ML	Thu Jul 08 18:35:44 1999 +0200
     4.2 +++ b/src/Pure/axclass.ML	Thu Jul 08 18:36:09 1999 +0200
     4.3 @@ -408,7 +408,7 @@
     4.4  fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
     4.5    thy
     4.6    |> IsarThy.theorem_i (("", [inst_attribute add_thms],
     4.7 -    (mk_prop (Theory.sign_of thy) sig_prop, [])), comment) int;
     4.8 +    (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
     4.9  
    4.10  val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
    4.11  val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;